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 );

I: now :: thesis: for x, y being object st x in the carrier of (Polynom-Ring F) & y in the carrier of (Polynom-Ring F) holds
ex z being object st
( z in the carrier of (Polynom-Ring F) & S₁[x,y,z] )

let x, y be object ; :: thesis: ( x in the carrier of (Polynom-Ring F) & y in the carrier of (Polynom-Ring F) implies ex z being object st
( z in the carrier of (Polynom-Ring F) & S₁[x,y,z] ) )
assume ( x in the carrier of (Polynom-Ring F) & y in the carrier of (Polynom-Ring F) ) ; :: thesis: ex z being object st
( z in the carrier of (Polynom-Ring F) & S₁[x,y,z] )
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: verum

proof

take s = (r *' q) mod p; :: thesis: ( s in the carrier of (Polynom-Ring F) & S₁[x,y,s] )
thus s in the carrier of (Polynom-Ring F) by POLYNOM3:def 10; :: thesis: S₁[x,y,s]
take xx ; :: thesis: ex q being Element of the carrier of (Polynom-Ring F) st
( x = xx & y = q & s = (xx *' q) mod p )
take yy ; :: thesis: ( x = xx & y = yy & s = (xx *' yy) mod p )
thus ( x = xx & y = yy & s = (xx *' yy) mod p ) ; :: thesis: verum

end;

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: for r, q being Polynomial of F holds f . (r,q) = (r *' q) mod p

now :: thesis: for r, q being Polynomial of F holds f . (r,q) = (r *' q) mod p

let r, q be Polynomial of F; :: thesis: f . (r,q) = (r *' q) mod p
( 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: verum

end;

hence for r, q being Polynomial of F holds f . (r,q) = (r *' q) mod p ; :: thesis: verum