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

proof

for x1, x2 being set st x1 in dom (canHom I) & x2 in dom (canHom I) & (canHom I) . x1 = (canHom I) . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom (canHom I) & x2 in dom (canHom I) & (canHom I) . x1 = (canHom I) . x2 implies x1 = x2 )
assume A2: ( x1 in dom (canHom I) & x2 in dom (canHom I) & (canHom I) . x1 = (canHom I) . x2 ) ; :: thesis: x1 = x2
then reconsider x1 = x1, x2 = x2 as Element of I ;
reconsider t1 = quotient x1,(1. I), t2 = quotient x2,(1. I) as Element of Q. I ;
A3: QClass. t1 = (canHom I) . x2 by A2, Def28
.= QClass. t2 by Def28 ;
t1 in QClass. t1 by Th6;
then A4: (t1 `1 ) * (t2 `2 ) = (t1 `2 ) * (t2 `1 ) by A3, Def4;
A5: t2 `2 = 1. I

proof

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

end;

A6: t1 `2 = 1. I

proof

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

end;

A7: t2 `1 = x2

proof

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

end;

t1 `1 = x1

proof

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

end;

then x1 = (t1 `2 ) * (t2 `1 ) by A4, A5, VECTSP_1:def 16
.= x2 by A6, A7, VECTSP_1:def 16 ;
hence x1 = x2 ; :: thesis: verum

end;

then A8: canHom I is one-to-one by FUNCT_1:def 8;
canHom I is RingHomomorphism by Th59;
hence canHom I is RingMonomorphism by A8, Def23; :: thesis: verum

end;

hence canHom I is RingMonomorphism ; :: thesis: verum