proposition: Lemma existence_point_fixe_g : a <> oneC -> exists J : PO, g J = J.
proof: Proof. intros. elim existence_point_fixe_complexe with (a := a) (b := b) (f := f); [ intros j H0; try clear existence_point_fixe_complexe; try exact H0 | auto | auto ]. exists (image j). rewrite g_def; rewrite transforme_image; rewrite H0; auto. try exact f_def. Qed.