A1:
[#] (ExField (x,o)) = carr (x,o)
by Def8;

defpred S_{1}[ object , object ] means ( ( $1 = x & $2 = o ) or ( $1 <> x & $2 = $1 ) );

A2: for u being object st u in [#] F holds

ex y being object st

( y in the carrier of (ExField (x,o)) & S_{1}[u,y] )

A6: for u being object st u in [#] F holds

S_{1}[u,g . u]
from FUNCT_2:sch 1(A2);

reconsider g = g as Function of F,(ExField (x,o)) ;

take g ; :: thesis: ( g . x = o & ( for a being Element of F st a <> x holds

g . a = a ) )

thus ( g . x = o & ( for a being Element of F st a <> x holds

g . a = a ) ) by A6; :: thesis: verum

defpred S

A2: for u being object st u in [#] F holds

ex y being object st

( y in the carrier of (ExField (x,o)) & S

proof

consider g being Function of ([#] F), the carrier of (ExField (x,o)) such that
let u be object ; :: thesis: ( u in [#] F implies ex y being object st

( y in the carrier of (ExField (x,o)) & S_{1}[u,y] ) )

assume A3: u in [#] F ; :: thesis: ex y being object st

( y in the carrier of (ExField (x,o)) & S_{1}[u,y] )

end;( y in the carrier of (ExField (x,o)) & S

assume A3: u in [#] F ; :: thesis: ex y being object st

( y in the carrier of (ExField (x,o)) & S

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

end;

suppose A4:
u = x
; :: thesis: ex y being object st

( y in the carrier of (ExField (x,o)) & S_{1}[u,y] )

( y in the carrier of (ExField (x,o)) & S

take b = o; :: thesis: ( b in the carrier of (ExField (x,o)) & S_{1}[u,b] )

o in {o} by TARSKI:def 1;

hence b in the carrier of (ExField (x,o)) by A1, XBOOLE_0:def 3; :: thesis: S_{1}[u,b]

thus S_{1}[u,b]
by A4; :: thesis: verum

end;o in {o} by TARSKI:def 1;

hence b in the carrier of (ExField (x,o)) by A1, XBOOLE_0:def 3; :: thesis: S

thus S

suppose A5:
u <> x
; :: thesis: ex y being object st

( y in the carrier of (ExField (x,o)) & S_{1}[u,y] )

( y in the carrier of (ExField (x,o)) & S

take
u
; :: thesis: ( u in the carrier of (ExField (x,o)) & S_{1}[u,u] )

not u in {x} by A5, TARSKI:def 1;

then u in ([#] F) \ {x} by A3, XBOOLE_0:def 5;

hence u in the carrier of (ExField (x,o)) by A1, XBOOLE_0:def 3; :: thesis: S_{1}[u,u]

thus S_{1}[u,u]
by A5; :: thesis: verum

end;not u in {x} by A5, TARSKI:def 1;

then u in ([#] F) \ {x} by A3, XBOOLE_0:def 5;

hence u in the carrier of (ExField (x,o)) by A1, XBOOLE_0:def 3; :: thesis: S

thus S

A6: for u being object st u in [#] F holds

S

reconsider g = g as Function of F,(ExField (x,o)) ;

take g ; :: thesis: ( g . x = o & ( for a being Element of F st a <> x holds

g . a = a ) )

thus ( g . x = o & ( for a being Element of F st a <> x holds

g . a = a ) ) by A6; :: thesis: verum