poly_mod p is linear

proof

thus ( poly_mod p is additive & poly_mod p is multiplicative & poly_mod p is unity-preserving ) ; :: according to RINGCAT1:def 1 :: thesis: verum

end;

hence Polynom-Ring p is Polynom-Ring F -homomorphic by RING_2:def 4; :: thesis: verum