let x1, y1 be Element of (Polynom-Ring F); :: thesis: ((poly_mod p) . x1) + ((poly_mod p) . y1) = (poly_mod p) . (x1 + y1)
reconsider x = x1, y = y1 as Element of the carrier of (Polynom-Ring F) ;
H: ( (poly_mod p) . x = x mod p & (poly_mod p) . y = y mod p ) by dpm;
then reconsider fx = (poly_mod p) . x, fy = (poly_mod p) . y as Element of (Polynom-Ring F) by POLYNOM3:def 10;
A3: [((poly_mod p) . x),((poly_mod p) . y)] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):] by ZFMISC_1:def 2;
thus ((poly_mod p) . x1) + ((poly_mod p) . y1) = ( the addF of (Polynom-Ring F) || the carrier of (Polynom-Ring p)) . (((poly_mod p) . x1),((poly_mod p) . y1)) by defprfp
.= fx + fy by A3, FUNCT_1:49
.= (x mod p) + (y mod p) by H, POLYNOM3:def 10
.= (x + y) mod p by div4
.= (poly_mod p) . (x + y) by dpm
.= (poly_mod p) . (x1 + y1) by POLYNOM3:def 10 ; :: thesis: verum

let x1, y1 be Element of (Polynom-Ring F); :: thesis: ((poly_mod p) . x1) * ((poly_mod p) . y1) = (poly_mod p) . (x1 * y1)
reconsider x = x1, y = y1 as Element of the carrier of (Polynom-Ring F) ;
H: ( (poly_mod p) . x = x mod p & (poly_mod p) . y = y mod p ) by dpm;
then reconsider fx = (poly_mod p) . x, fy = (poly_mod p) . y as Element of (Polynom-Ring F) by POLYNOM3:def 10;
A3: [((poly_mod p) . x),((poly_mod p) . y)] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):] by ZFMISC_1:def 2;
thus ((poly_mod p) . x1) * ((poly_mod p) . y1) = ((poly_mult_mod p) || the carrier of (Polynom-Ring p)) . (((poly_mod p) . x1),((poly_mod p) . y1)) by defprfp
.= (poly_mult_mod p) . (((poly_mod p) . x),((poly_mod p) . y)) by A3, FUNCT_1:49
.= ((x mod p) *' (y mod p)) mod p by H, defpmm
.= (x *' y) mod p by div3a
.= (poly_mod p) . (x *' y) by dpm
.= (poly_mod p) . (x1 * y1) by POLYNOM3:def 10 ; :: thesis: verum