Section p71E2.

A morphism from a free monoid to the natural numbers

Let A:CSetoid.

Variable A:CSetoid.

Let L: (free_monoid_as_CMonoid A)-> nat_as_CMonoid.
Defined.

Lemma L_strext: (fun_strext L).

Definition L_as_CSetoid_fun:=
(Build_CSetoid_fun _ _ L L_strext).

Lemma L_is_morphism: (morphism _ _ L_as_CSetoid_fun).

End p71E2.