set f = canHom R;
hereby :: according to VECTSP_1:def 19 :: thesis: ( canHom R is multiplicative & canHom R is unity-preserving )
let x, y be Element of R; :: thesis: ((canHom R) . x) + ((canHom R) . y) = (canHom R) . (x + y)
( (canHom R) . x = x | R & (canHom R) . y = y | R ) by defcanhom;
hence ((canHom R) . x) + ((canHom R) . y) = (x | R) + (y | R) by POLYNOM3:def 10
.= (x + y) | R by T4a
.= (canHom R) . (x + y) by defcanhom ;
:: thesis: verum
end;
hereby :: according to GROUP_6:def 6 :: thesis: canHom R is unity-preserving
let x, y be Element of R; :: thesis: ((canHom R) . x) * ((canHom R) . y) = (canHom R) . (x * y)
( (canHom R) . x = x | R & (canHom R) . y = y | R ) by defcanhom;
hence ((canHom R) . x) * ((canHom R) . y) = (x | R) *' (y | R) by POLYNOM3:def 10
.= (x * y) | R by T4
.= (canHom R) . (x * y) by defcanhom ;
:: thesis: verum
end;
thus (canHom R) . (1_ R) = (1. R) | R by defcanhom
.= 1_. R
.= 1_ (Polynom-Ring R) by POLYNOM3:def 10 ; :: according to GROUP_1:def 13 :: thesis: verum