let I be non degenerated commutative domRing-like Ring; :: thesis: canHom I is RingHomomorphism
A1: 0. I <> 1. I ;
for x, y being Element of I holds
( (canHom I) . (x + y) = ((canHom I) . x) + ((canHom I) . y) & (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )

proof

reconsider res3 = [(1. I),(1. I)] as Element of Q. I by A1, Def1;
let x, y be Element of I; :: thesis: ( (canHom I) . (x + y) = ((canHom I) . x) + ((canHom I) . y) & (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )
reconsider t1 = quotient (x,(1. I)), t2 = quotient (y,(1. I)) as Element of Q. I ;
A2: t1 `2 = [x,(1. I)] `2 by A1, Def27
.= 1. I by MCART_1:def 2 ;
( t1 `2 <> 0. I & t2 `2 <> 0. I ) by Th2;
then A3: (t1 `2) * (t2 `2) <> 0. I by VECTSP_2:def 1;
then reconsider sum = [(((t1 `1) * (t2 `2)) + ((t2 `1) * (t1 `2))),((t1 `2) * (t2 `2))] as Element of Q. I by Def1;
A4: t2 `1 = [y,(1. I)] `1 by A1, Def27
.= y by MCART_1:def 1 ;
reconsider prod = [((t1 `1) * (t2 `1)),((t1 `2) * (t2 `2))] as Element of Q. I by A3, Def1;
A5: ( QClass. t1 = (canHom I) . x & QClass. t2 = (canHom I) . y ) by Def28;
A6: (quotadd I) . ((QClass. t1),(QClass. t2)) = qadd ((QClass. t1),(QClass. t2)) by Def12
.= QClass. (padd (t1,t2)) by Th11
.= QClass. sum ;
A7: t1 `1 = [x,(1. I)] `1 by A1, Def27
.= x by MCART_1:def 1 ;
A8: t2 `2 = [y,(1. I)] `2 by A1, Def27
.= 1. I by MCART_1:def 2 ;
then A9: sum = [((t1 `1) + ((t2 `1) * (1. I))),((1. I) * (1. I))] by A2, VECTSP_1:def 6
.= [((t1 `1) + (t2 `1)),((1. I) * (1. I))] by VECTSP_1:def 6
.= [(x + y),(1. I)] by A4, A7, VECTSP_1:def 6 ;
thus (canHom I) . (x + y) = QClass. (quotient ((x + y),(1. I))) by Def28
.= ((canHom I) . x) + ((canHom I) . y) by A1, A5, A6, A9, Def27 ; :: thesis: ( (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )
A10: (quotmult I) . ((QClass. t1),(QClass. t2)) = qmult ((QClass. t1),(QClass. t2)) by Def13
.= QClass. (pmult (t1,t2)) by Th12
.= QClass. prod ;
A11: prod = [(x * y),(1. I)] by A8, A2, A4, A7, VECTSP_1:def 6;
thus (canHom I) . (x * y) = QClass. (quotient ((x * y),(1. I))) by Def28
.= ((canHom I) . x) * ((canHom I) . y) by A1, A5, A10, A11, Def27 ; :: thesis: (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I)
A12: for u being set st u in QClass. res3 holds
u in q1. I

proof

let u be set ; :: thesis: ( u in QClass. res3 implies u in q1. I )
assume A13: u in QClass. res3 ; :: thesis: u in q1. I
then reconsider u = u as Element of Q. I ;
u `1 = (u `1) * (1. I) by VECTSP_1:def 6
.= (u `1) * (res3 `2) by MCART_1:def 2
.= (u `2) * (res3 `1) by A13, Def4
.= (u `2) * (1. I) by MCART_1:def 1
.= u `2 by VECTSP_1:def 6 ;
hence u in q1. I by Def9; :: thesis: verum

end;

for u being set st u in q1. I holds
u in QClass. res3

proof

let u be set ; :: thesis: ( u in q1. I implies u in QClass. res3 )
assume A14: u in q1. I ; :: thesis: u in QClass. res3
then reconsider u = u as Element of Q. I ;
(u `1) * (res3 `2) = (u `1) * (1. I) by MCART_1:def 2
.= u `1 by VECTSP_1:def 6
.= u `2 by A14, Def9
.= (u `2) * (1. I) by VECTSP_1:def 6
.= (u `2) * (res3 `1) by MCART_1:def 1 ;
hence u in QClass. res3 by Def4; :: thesis: verum

end;

then A15: q1. I = QClass. res3 by A12, TARSKI:1;
thus (canHom I) . (1_ I) = QClass. (quotient ((1. I),(1. I))) by Def28
.= 1_ (the_Field_of_Quotients I) by A1, A15, Def27 ; :: thesis: verum

end;

then ( canHom I is additive & canHom I is multiplicative & canHom I is unity-preserving ) by GRCAT_1:def 8, GROUP_1:def 13, GROUP_6:def 6;
hence canHom I is RingHomomorphism ; :: thesis: verum