set B = Polynom-Ring (n,R);
let g1, g2 be Function of R,(Polynom-Ring (n,R)); :: thesis: ( ( for a being Element of R holds g1 . a = a | (n,R) ) & ( for a being Element of R holds g2 . a = a | (n,R) ) implies g1 = g2 )
assume that
A1: for a being Element of R holds g1 . a = a | (n,R) and
A2: for a being Element of R holds g2 . a = a | (n,R) ; :: thesis: g1 = g2
A: dom g1 = the carrier of R 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 a = x as Element of R ;
thus g1 . x = a | (n,R) by A1
.= g2 . x by A2 ; :: thesis: verum

end;

hence g1 = g2 by A; :: thesis: verum