set B = Polynom-Ring F;
let g1, g2 be BinOp of (Polynom-Ring F); ( ( 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
; 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
;
hence
g1 = g2
by A, FUNCT_1:2; verum