set B = Polynom-Ring F;
let g1, g2 be BinOp of (Polynom-Ring F); :: thesis: ( ( for r, q being Polynomial of F holds g1 . (r,q) = (r *' q) mod p ) & ( for r, q being Polynomial of F holds g2 . (r,q) = (r *' q) mod p ) implies g1 = g2 )
assume that
A1: for r, q being Polynomial of F holds g1 . (r,q) = (r *' q) mod p and
A2: for r, q being Polynomial of F holds g2 . (r,q) = (r *' q) mod p ; :: thesis: g1 = g2
A: dom g1 = [: the carrier of (Polynom-Ring F), the carrier of (Polynom-Ring F):] by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom g1 holds
g1 . x = g2 . x

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume x in dom g1 ; :: thesis: g1 . x = g2 . x
then consider r, q being object such that
H: ( r in the carrier of (Polynom-Ring F) & q in the carrier of (Polynom-Ring F) & x = [r,q] ) by ZFMISC_1:def 2;
reconsider r = r, q = q as Polynomial of F by H, POLYNOM3:def 10;
thus g1 . x = g1 . (r,q) by H
.= (r *' q) mod p by A1
.= g2 . (r,q) by A2
.= g2 . x by H ; :: thesis: verum

end;

hence g1 = g2 by A, FUNCT_1:2; :: thesis: verum