set f = canHom (n,R);

now :: thesis: for x1, x2 being object st x1 in the carrier of R & x2 in the carrier of R & (canHom (n,R)) . x1 = (canHom (n,R)) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in the carrier of R & x2 in the carrier of R & (canHom (n,R)) . x1 = (canHom (n,R)) . x2 implies x1 = x2 )
assume AS: ( x1 in the carrier of R & x2 in the carrier of R & (canHom (n,R)) . x1 = (canHom (n,R)) . x2 ) ; :: thesis: x1 = x2
then reconsider a = x1, b = x2 as Element of R ;
a | (n,R) = (canHom (n,R)) . x2 by AS, defcanhom
.= b | (n,R) by defcanhom ;
hence x1 = x2 by POLYNOM7:21; :: thesis: verum

end;

then canHom (n,R) is one-to-one by FUNCT_2:19;
hence canHom (n,R) is monomorphism ; :: thesis: verum