let g1, g2 be Function of F,(ExField (x,o)); :: thesis: ( g1 . x = o & ( for a being Element of F st a <> x holds
g1 . a = a ) & g2 . x = o & ( for a being Element of F st a <> x holds
g2 . a = a ) implies g1 = g2 )
assume that
A7: ( g1 . x = o & ( for a being Element of F st a <> x holds
g1 . a = a ) ) and
A8: ( g2 . x = o & ( for a being Element of F st a <> x holds
g2 . a = a ) ) ; :: thesis: g1 = g2

now :: thesis: for o being object st o in [#] F holds
g1 . o = g2 . o

let o be object ; :: thesis: ( o in [#] F implies g1 . b₁ = g2 . b₁ )
assume o in [#] F ; :: thesis: g1 . b₁ = g2 . b₁
then reconsider a = o as Element of F ;

per cases ( a = x or a <> x ) ;

suppose a = x ; :: thesis: g1 . b₁ = g2 . b₁

hence g1 . o = g2 . o by A8, A7; :: thesis: verum

end;

suppose A9: a <> x ; :: thesis: g1 . b₁ = g2 . b₁

then g1 . a = a by A7
.= g2 . a by A9, A8 ;
hence g1 . o = g2 . o ; :: thesis: verum

end;

end;

end;

hence g1 = g2 ; :: thesis: verum