let I be non degenerated commutative domRing-like Ring; :: thesis: canHom I is RingMonomorphism
A1: 0. I <> 1. I ;
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 that
A2: ( x1 in dom (canHom I) & x2 in dom (canHom I) ) and
A3: (canHom I) . x1 = (canHom I) . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of I by A2;
reconsider t1 = quotient (x1,(1. I)), t2 = quotient (x2,(1. I)) as Element of Q. I ;
A4: t1 in QClass. t1 by Th6;
QClass. t1 = (canHom I) . x2 by A3, Def28
.= QClass. t2 by Def28 ;
then A5: (t1 `1) * (t2 `2) = (t1 `2) * (t2 `1) by A4, Def4;
A6: t1 `2 = [x1,(1. I)] `2 by A1, Def27
.= 1. I by MCART_1:def 2 ;
A7: t1 `1 = [x1,(1. I)] `1 by A1, Def27
.= x1 by MCART_1:def 1 ;
A8: t2 `1 = [x2,(1. I)] `1 by A1, Def27
.= x2 by MCART_1:def 1 ;
t2 `2 = [x2,(1. I)] `2 by A1, Def27
.= 1. I by MCART_1:def 2 ;
then x1 = (t1 `2) * (t2 `1) by A5, A7, VECTSP_1:def 6
.= x2 by A6, A8, VECTSP_1:def 6 ;
hence x1 = x2 ; :: thesis: verum

end;

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