A function from the natural numbers to a cyclic monoid
Let M:CMonoid, c:M and is_generated_by: forall(m:M),{n:nat | (power_CMonoid c n)≡m}.Variable M:CMonoid.
Variable c:M.
Definition power_CMonoid_CSetoid: M-> nat_as_CSetoid -> M.
Defined.
Variable is_generated_by: forall(m:M),{n:nat | (power_CMonoid c n)[=]m}.
Let f:= fun (H:forall(m:M),{n:nat | (power_CMonoid c n)[=]m})=>
fun (n:nat_as_CMonoid)=> power_CMonoid c n.
Lemma f_strext: (fun_strext (f is_generated_by)).
Definition f_as_CSetoid_fun:=
(Build_CSetoid_fun nat_as_CMonoid M (f is_generated_by) f_strext).
Lemma surjective_f: (surjective f_as_CSetoid_fun).
End p71E1.