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 . b1 = g2 . b1 )
assume o in [#] F ; :: thesis: g1 . b1 = g2 . b1
then reconsider a = o as Element of F ;
per cases ( a = x or a <> x ) ;
suppose a = x ; :: thesis: g1 . b1 = g2 . b1
hence g1 . o = g2 . o by A8, A7; :: thesis: verum
end;
suppose A9: a <> x ; :: thesis: g1 . b1 = g2 . b1
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