set R = F;

set B = Polynom-Ring p;

let g1, g2 be Function of F,(Polynom-Ring p); :: thesis: ( ( for a being Element of F holds g1 . a = a | F ) & ( for a being Element of F holds g2 . a = a | F ) implies g1 = g2 )

assume that

A1: for a being Element of F holds g1 . a = a | F and

A2: for a being Element of F holds g2 . a = a | F ; :: thesis: g1 = g2

A: dom g1 = the carrier of F by FUNCT_2:def 1

.= dom g2 by FUNCT_2:def 1 ;

set B = Polynom-Ring p;

let g1, g2 be Function of F,(Polynom-Ring p); :: thesis: ( ( for a being Element of F holds g1 . a = a | F ) & ( for a being Element of F holds g2 . a = a | F ) implies g1 = g2 )

assume that

A1: for a being Element of F holds g1 . a = a | F and

A2: for a being Element of F holds g2 . a = a | F ; :: thesis: g1 = g2

A: dom g1 = the carrier of 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

hence
g1 = g2
by A; :: thesis: verumg1 . 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 F ;

thus g1 . x = a | F by A1

.= g2 . x by A2 ; :: thesis: verum

end;assume x in dom g1 ; :: thesis: g1 . x = g2 . x

then reconsider a = x as Element of F ;

thus g1 . x = a | F by A1

.= g2 . x by A2 ; :: thesis: verum