let I be non degenerated commutative domRing-like Ring; :: thesis: canHom I is embedding
A1: 0. I <> 1. I ;
for x1, x2 being object 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 object ; :: 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 Th5;
QClass. t1 = (canHom I) . x2 by A3, Def21
.= QClass. t2 by Def21 ;
then A5: (t1 `1) * (t2 `2) = (t1 `2) * (t2 `1) by A4, Def4;
A6: t1 `2 = [x1,(1. I)] `2 by A1, Def20
.= 1. I ;
A7: t1 `1 = [x1,(1. I)] `1 by A1, Def20
.= x1 ;
A8: t2 `1 = [x2,(1. I)] `1 by A1, Def20
.= x2 ;
t2 `2 = [x2,(1. I)] `2 by A1, Def20
.= 1. I ;
then x1 = (t1 `2) * (t2 `1) by A5, A7
.= x2 by A6, A8 ;
hence x1 = x2 ; :: thesis: verum

end;

then A9: canHom I is one-to-one by FUNCT_1:def 4;
canHom I is RingHomomorphism by Th56;
hence canHom I is embedding by A9; :: thesis: verum