set B = Polynom-Ring F;
set D = the carrier of (Polynom-Ring F);
defpred S₁[ object , object , object ] means ex r, q being Element of the carrier of (Polynom-Ring F) st
( $1 = r & $2 = q & $3 = (r *' q) mod p );

let x, y be object ; :: thesis:
assume ( x in the carrier of (Polynom-Ring F) & y in the carrier of (Polynom-Ring F) ) ; :: thesis:
then reconsider xx = x, yy = y as Element of the carrier of (Polynom-Ring F) ;
reconsider r = xx, q = yy as Polynomial of F ;
thus ex z being object st
( z in the carrier of (Polynom-Ring F) & S₁[x,y,z] ) :: thesis:

take s = (r *' q) mod p; :: thesis:
thus s in the carrier of (Polynom-Ring F) by POLYNOM3:def 10; :: thesis:
take xx ; :: thesis:
take yy ; :: thesis:
thus ( x = xx & y = yy & s = (xx *' yy) mod p ) ; :: thesis:

end;

consider f being Function of [: the carrier of (Polynom-Ring F), the carrier of (Polynom-Ring F):], the carrier of (Polynom-Ring F) such that
H: for x, y being object st x in the carrier of (Polynom-Ring F) & y in the carrier of (Polynom-Ring F) holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 1(I);
take f ; :: thesis:

let r, q be Polynomial of F; :: thesis:
( r in the carrier of (Polynom-Ring F) & q in the carrier of (Polynom-Ring F) ) by POLYNOM3:def 10;
then S₁[r,q,f . (r,q)] by H;
then consider rr, qq being Element of the carrier of (Polynom-Ring F) such that
K: ( rr = r & qq = q & f . (rr,qq) = (rr *' qq) mod p ) ;
thus f . (r,q) = (r *' q) mod p by K; :: thesis:

end;