set R = F;
set RX = Polynom-Ring F;
set f = canHomP p;
set B = Polynom-Ring p;

hereby :: according to VECTSP_1:def 19 :: thesis: ( canHomP p is multiplicative & canHomP p is unity-preserving & canHomP p is one-to-one )

let x, y be Element of F; :: thesis: ((canHomP p) . x) + ((canHomP p) . y) = (canHomP p) . (x + y)
B: ( (canHomP p) . x = x | F & (canHomP p) . y = y | F ) by defch;
A: [((canHomP p) . x),((canHomP p) . y)] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):] by ZFMISC_1:def 2;
reconsider fx = (canHomP p) . x, fy = (canHomP p) . y as Element of the carrier of (Polynom-Ring F) by B, POLYNOM3:def 10;
thus ((canHomP p) . x) + ((canHomP p) . y) = ( the addF of (Polynom-Ring F) || the carrier of (Polynom-Ring p)) . (((canHomP p) . x),((canHomP p) . y)) by RING_4:def 8
.= fx + fy by A, FUNCT_1:49
.= (x | F) + (y | F) by B, POLYNOM3:def 10
.= (x + y) | F by RING_4:17
.= (canHomP p) . (x + y) by defch ; :: thesis: verum

end;

hereby :: according to GROUP_6:def 6 :: thesis: ( canHomP p is unity-preserving & canHomP p is one-to-one )

let x, y be Element of F; :: thesis: ((canHomP p) . x) * ((canHomP p) . y) = (canHomP p) . (x * y)
B: ( (canHomP p) . x = x | F & (canHomP p) . y = y | F ) by defch;
A: [((canHomP p) . x),((canHomP p) . y)] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):] by ZFMISC_1:def 2;
reconsider fx = (canHomP p) . x, fy = (canHomP p) . y as Element of the carrier of (Polynom-Ring F) by B, POLYNOM3:def 10;
reconsider p1 = p as Polynomial of F ;
C: ( deg ((x * y) | F) <= 0 & deg p > 0 ) by RING_4:def 4, RATFUNC1:def 2;
thus ((canHomP p) . x) * ((canHomP p) . y) = ((poly_mult_mod p) || the carrier of (Polynom-Ring p)) . (((canHomP p) . x),((canHomP p) . y)) by RING_4:def 8
.= (poly_mult_mod p) . (fx,fy) by A, FUNCT_1:49
.= ((x | F) *' (y | F)) mod p by B, RING_4:def 7
.= ((x * y) | F) mod p by RING_4:18
.= (x * y) | F by C, RING_4:2
.= (canHomP p) . (x * y) by defch ; :: thesis: verum

end;

thus (canHomP p) . (1_ F) = (1. F) | F by defch
.= 1_. F by RING_4:14
.= 1_ (Polynom-Ring p) by RING_4:def 8 ; :: according to GROUP_1:def 13 :: thesis: canHomP p is one-to-one

now :: thesis: for x1, x2 being object st x1 in the carrier of F & x2 in the carrier of F & (canHomP p) . x1 = (canHomP p) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in the carrier of F & x2 in the carrier of F & (canHomP p) . x1 = (canHomP p) . x2 implies x1 = x2 )
assume AS: ( x1 in the carrier of F & x2 in the carrier of F & (canHomP p) . x1 = (canHomP p) . x2 ) ; :: thesis: x1 = x2
then reconsider a = x1, b = x2 as Element of F ;
a | F = (canHomP p) . x2 by AS, defch
.= b | F by defch ;
hence x1 = x2 by RING_4:19; :: thesis: verum

end;

hence canHomP p is one-to-one by FUNCT_2:19; :: thesis: verum