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

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

hence
g1 = g2
; :: thesis: verumg1 . o = g2 . o

let o be object ; :: thesis: ( o in [#] F implies g1 . b_{1} = g2 . b_{1} )

assume o in [#] F ; :: thesis: g1 . b_{1} = g2 . b_{1}

then reconsider a = o as Element of F ;

end;assume o in [#] F ; :: thesis: g1 . b

then reconsider a = o as Element of F ;