set B = Polynom-Ring F;
let g1, g2 be Function of (Polynom-Ring F),(Polynom-Ring p); :: thesis: ( ( for q being Polynomial of F holds g1 . q = q mod p ) & ( for q being Polynomial of F holds g2 . q = q mod p ) implies g1 = g2 )
assume that
A1: for q being Polynomial of F holds g1 . q = q mod p and
A2: for q being Polynomial of F holds g2 . q = q mod p ; :: thesis: g1 = g2
A: dom g1 = 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 reconsider q = x as Polynomial of F by POLYNOM3:def 10;
thus g1 . x = q mod p by A1
.= g2 . x by A2 ; :: thesis: verum

end;

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