set f = canHom R;
A: canHom R is linear by RINGCAT1:def 1;
now :: thesis: for x1, x2 being object st x1 in the carrier of R & x2 in the carrier of R & (canHom R) . x1 = (canHom R) . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in the carrier of R & x2 in the carrier of R & (canHom R) . x1 = (canHom R) . x2 implies x1 = x2 )
assume AS: ( x1 in the carrier of R & x2 in the carrier of R & (canHom R) . x1 = (canHom R) . x2 ) ; :: thesis: x1 = x2
then reconsider a = x1, b = x2 as Element of R ;
a | R = (canHom R) . x2 by AS, defcanhom
.= b | R by defcanhom ;
hence x1 = x2 by T9; :: thesis: verum
end;
then canHom R is one-to-one by FUNCT_2:19;
hence canHom R is RingMonomorphism by A; :: thesis: verum