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