A1: [#] (ExField (x,o)) = carr (x,o) by Def8;
defpred S₁[ 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₁[u,y] )

proof

let u be object ; :: thesis: ( u in [#] F implies ex y being object st
( y in the carrier of (ExField (x,o)) & S₁[u,y] ) )
assume A3: u in [#] F ; :: thesis: ex y being object st
( y in the carrier of (ExField (x,o)) & S₁[u,y] )

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

suppose A4: u = x ; :: thesis: ex y being object st
( y in the carrier of (ExField (x,o)) & S₁[u,y] )

take b = o; :: thesis: ( b in the carrier of (ExField (x,o)) & S₁[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₁[u,b]
thus S₁[u,b] by A4; :: thesis: verum

end;

suppose A5: u <> x ; :: thesis: ex y being object st
( y in the carrier of (ExField (x,o)) & S₁[u,y] )

take u ; :: thesis: ( u in the carrier of (ExField (x,o)) & S₁[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₁[u,u]
thus S₁[u,u] by A5; :: thesis: verum

end;

end;

end;

consider g being Function of ([#] F), the carrier of (ExField (x,o)) such that
A6: for u being object st u in [#] F holds
S₁[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