proposition: Theorem f12_strong_ext : fun_strext f12.
proof: Proof. intros. red in |- *. unfold f12 in |- *. intros x y H. case (ap_imp_less R2 (Lim (image_G_as_CauchySeq12 x)) (Lim (image_G_as_CauchySeq12 y)) H). intro. apply less_imp_ap. apply less_wdl with (x := Lim (inj_Q_G_as_CauchySeq R1 x)). apply less_wdr with (y := Lim (inj_Q_G_as_CauchySeq R1 y)). apply Lim_pres_less. unfold inj_Q_G_as_CauchySeq in |- *. change ((Build_CauchySeq R1 (fun m : nat => inj_Q R1 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 x) m)) (inj_Q_Cauchy R1 (G_as_CauchySeq R1 x)) :R_COrdField R1)[<] Build_CauchySeq R1 (fun n : nat => inj_Q R1 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 y) n)) (inj_Q_Cauchy R1 (G_as_CauchySeq R1 y))) in |- *. apply inj_seq_less. apply less_inj_seq with (IR := R2). change ((image_G_as_CauchySeq12 x:R_COrdField R2)[<] (image_G_as_CauchySeq12 y:R_COrdField R2)) in |- *. apply less_pres_Lim. assumption. apply eq_symmetric_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. apply eq_symmetric_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. intro. apply Greater_imp_ap. apply less_wdl with (x := Lim (inj_Q_G_as_CauchySeq R1 y)). apply less_wdr with (y := Lim (inj_Q_G_as_CauchySeq R1 x)). apply Lim_pres_less. unfold inj_Q_G_as_CauchySeq in |- *. change ((Build_CauchySeq R1 (fun m : nat => inj_Q R1 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 y) m)) (inj_Q_Cauchy R1 (G_as_CauchySeq R1 y)) :R_COrdField R1)[<] Build_CauchySeq R1 (fun n : nat => inj_Q R1 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 x) n)) (inj_Q_Cauchy R1 (G_as_CauchySeq R1 x))) in |- *. apply inj_seq_less. apply less_inj_seq with (IR := R2). change ((image_G_as_CauchySeq12 y:R_COrdField R2)[<] (image_G_as_CauchySeq12 x:R_COrdField R2)) in |- *. apply less_pres_Lim. assumption. apply eq_symmetric_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. apply eq_symmetric_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism