proposition: Theorem f12_pres_mult : fun_pres_bin_fun R1 R2 f12 (cr_mult (c:=R1)) (cr_mult (c:=R2)).
proof: Proof. red in |- *. intros. unfold f12 in |- *. apply eq_transitive_unfolded with (y := Lim ((image_G_as_CauchySeq12 x:R_COrdField R2)[*] image_G_as_CauchySeq12 y)). apply Lim_well_def. unfold image_G_as_CauchySeq12 in |- *. apply eq_transitive_unfolded with (S := R_COrdField R2:CSetoid) (y := Build_CauchySeq R2 (fun m : nat => inj_Q R2 (G R1 x m[*]G R1 y m)) (inj_Q_Cauchy R2 (Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 x m[*]G R1 y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof _ (G_as_CauchySeq R1 x)) (CS_proof _ (G_as_CauchySeq R1 y))))) :R_COrdField R2). change ((Build_CauchySeq R2 (fun n : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 (x[*]y)) n)) (inj_Q_Cauchy R2 (G_as_CauchySeq R1 (x[*]y))) :R_COrdField R2)[=] Build_CauchySeq R2 (fun m : nat => inj_Q R2 (CS_seq Q_as_COrdField (Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 x m[*]G R1 y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof _ (G_as_CauchySeq R1 x)) (CS_proof _ (G_as_CauchySeq R1 y)))) m)) (inj_Q_Cauchy R2 (Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 x m[*]G R1 y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof _ (G_as_CauchySeq R1 x)) (CS_proof _ (G_as_CauchySeq R1 y)))))) in |- *. apply inj_seq_well_def. unfold G_as_CauchySeq in |- *. change ((Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 (x[*]y) m) (CS_seq_G R1 (x[*]y)) :R_COrdField Q_as_COrdField)[=] Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 x m[*]G R1 y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof _ (G_as_CauchySeq R1 x)) (CS_proof _ (G_as_CauchySeq R1 y)))) in |- *. apply G_pres_mult. apply not_ap_imp_eq. apply Eq_alt_2_2 with (x := Build_CauchySeq R2 (fun m : nat => inj_Q R2 (G R1 x m[*]G R1 y m)) (inj_Q_Cauchy R2 (Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 x m[*]G R1 y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof Q_as_COrdField (G_as_CauchySeq R1 x)) (CS_proof Q_as_COrdField (G_as_CauchySeq R1 y)))))) (y := Build_CauchySeq R2 (fun m : nat => inj_Q R2 (G R1 x m)[*]inj_Q R2 (G R1 y m)) (CS_seq_mult R2 _ _ (CS_proof R2 (image_G_as_CauchySeq12 x)) (CS_proof R2 (image_G_as_CauchySeq12 y)))). intros. exists 0. intros. unfold CS_seq in |- *. apply AbsSmall_wdr_unfolded with (y := [0]:R2). split. rstepr ([--]([0]:R2)). apply inv_resp_leEq. apply less_leEq. assumption. apply less_leEq. assumption. apply cg_cancel_rht with (x := inj_Q R2 (G R1 x m)[*]inj_Q R2 (G R1 y m)). astepl (inj_Q R2 (G R1 x m)[*]inj_Q R2 (G R1 y m)). apply eq_transitive_unfolded with (y := inj_Q R2 (G R1 x m[*]G R1 y m)). apply eq_symmetric_unfolded. apply inj_Q_mult. apply cg_cancel_mixed. apply Lim_pres_mult. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism