set f = canHom (n,R);

hereby :: according to VECTSP_1:def 19 :: thesis: ( canHom (n,R) is multiplicative & canHom (n,R) is unity-preserving )

let x, y be Element of R; :: thesis: ((canHom (n,R)) . x) + ((canHom (n,R)) . y) = (canHom (n,R)) . (x + y)
( (canHom (n,R)) . x = x | (n,R) & (canHom (n,R)) . y = y | (n,R) ) by defcanhom;
hence ((canHom (n,R)) . x) + ((canHom (n,R)) . y) = (x | (n,R)) + (y | (n,R)) by POLYNOM1:def 11
.= (x + y) | (n,R) by T4a
.= (canHom (n,R)) . (x + y) by defcanhom ;
:: thesis: verum

end;

hereby :: according to GROUP_6:def 6 :: thesis: canHom (n,R) is unity-preserving

let x, y be Element of R; :: thesis: ((canHom (n,R)) . x) * ((canHom (n,R)) . y) = (canHom (n,R)) . (x * y)
( (canHom (n,R)) . x = x | (n,R) & (canHom (n,R)) . y = y | (n,R) ) by defcanhom;
hence ((canHom (n,R)) . x) * ((canHom (n,R)) . y) = (x | (n,R)) *' (y | (n,R)) by POLYNOM1:def 11
.= (x * y) | (n,R) by T4
.= (canHom (n,R)) . (x * y) by defcanhom ;
:: thesis: verum

end;

thus (canHom (n,R)) . (1_ R) = (1. R) | (n,R) by defcanhom
.= 1_ (n,R) by POLYNOM7:20
.= 1_ (Polynom-Ring (n,R)) by POLYNOM1:def 11 ; :: according to GROUP_1:def 13 :: thesis: verum