let I be non degenerated commutative domRing-like Ring; :: thesis: canHom I is RingHomomorphism
A1: 0. I <> 1. I ;
canHom I is RingHomomorphism

proof

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

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: QClass. t1 = (canHom I) . x by Def28;
A3: QClass. t2 = (canHom I) . y by Def28;
( t1 `2 <> 0. I & t2 `2 <> 0. I ) by Th2;
then A4: (t1 `2 ) * (t2 `2 ) <> 0. I by VECTSP_2:def 5;
then reconsider sum = [(((t1 `1 ) * (t2 `2 )) + ((t2 `1 ) * (t1 `2 ))),((t1 `2 ) * (t2 `2 ))] as Element of Q. I by Def1;
A5: (quotadd I) . (QClass. t1),(QClass. t2) = qadd (QClass. t1),(QClass. t2) by Def12
.= QClass. (padd t1,t2) by Th11
.= QClass. sum ;
A6: t2 `2 = 1. I

proof

thus t2 `2 = [y,(1. I)] `2 by A1, Def27
.= 1. I by MCART_1:def 2 ; :: thesis: verum

end;

A7: t1 `2 = 1. I

proof

thus t1 `2 = [x,(1. I)] `2 by A1, Def27
.= 1. I by MCART_1:def 2 ; :: thesis: verum

end;

A8: t2 `1 = y

proof

thus t2 `1 = [y,(1. I)] `1 by A1, Def27
.= y by MCART_1:def 1 ; :: thesis: verum

end;

A9: t1 `1 = x

proof

thus t1 `1 = [x,(1. I)] `1 by A1, Def27
.= x by MCART_1:def 1 ; :: thesis: verum

end;

A10: sum = [((t1 `1 ) + ((t2 `1 ) * (1. I))),((1. I) * (1. I))] by A6, A7, VECTSP_1:def 16
.= [((t1 `1 ) + (t2 `1 )),((1. I) * (1. I))] by VECTSP_1:def 16
.= [(x + y),(1. I)] by A8, A9, VECTSP_1:def 16 ;
thus (canHom I) . (x + y) = QClass. (quotient (x + y),(1. I)) by Def28
.= ((canHom I) . x) + ((canHom I) . y) by A1, A2, A3, A5, A10, Def27 ; :: thesis: ( (canHom I) . (x * y) = ((canHom I) . x) * ((canHom I) . y) & (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I) )
reconsider prod = [((t1 `1 ) * (t2 `1 )),((t1 `2 ) * (t2 `2 ))] as Element of Q. I by A4, Def1;
A11: (quotmult I) . (QClass. t1),(QClass. t2) = qmult (QClass. t1),(QClass. t2) by Def13
.= QClass. (pmult t1,t2) by Th12
.= QClass. prod ;
A12: prod = [(x * y),(1. I)] by A6, A7, A8, A9, VECTSP_1:def 16;
thus (canHom I) . (x * y) = QClass. (quotient (x * y),(1. I)) by Def28
.= ((canHom I) . x) * ((canHom I) . y) by A1, A2, A3, A11, A12, Def27 ; :: thesis: (canHom I) . (1_ I) = 1_ (the_Field_of_Quotients I)
reconsider res3 = [(1. I),(1. I)] as Element of Q. I by A1, Def1;
A13: q1. I = QClass. res3

proof

A14: 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 A15: 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 16
.= u `2 by A15, Def9
.= (u `2 ) * (1. I) by VECTSP_1:def 16
.= (u `2 ) * (res3 `1 ) by MCART_1:def 1 ;
hence u in QClass. res3 by Def4; :: thesis: verum

end;

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 A16: 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 16
.= (u `1 ) * (res3 `2 ) by MCART_1:def 2
.= (u `2 ) * (res3 `1 ) by A16, Def4
.= (u `2 ) * (1. I) by MCART_1:def 1
.= u `2 by VECTSP_1:def 16 ;
hence u in q1. I by Def9; :: thesis: verum

end;

hence q1. I = QClass. res3 by A14, TARSKI:2; :: thesis: verum

end;

thus (canHom I) . (1_ I) = QClass. (quotient (1. I),(1. I)) by Def28
.= 1_ (the_Field_of_Quotients I) by A1, A13, Def27 ; :: thesis: verum

end;

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

end;

hence canHom I is RingHomomorphism ; :: thesis: verum