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

assume A3: u in [#] F ; :: thesis: ex y being object st
( y in the carrier of (ExField (x,o)) & S1[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)) & S1[u,y] )

take b = o; :: thesis: ( b in the carrier of (ExField (x,o)) & S1[u,b] )
o in {o} by TARSKI:def 1;
hence b in the carrier of (ExField (x,o)) by ; :: thesis: S1[u,b]
thus S1[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)) & S1[u,y] )

take u ; :: thesis: ( u in the carrier of (ExField (x,o)) & S1[u,u] )
not u in {x} by ;
then u in ([#] F) \ {x} by ;
hence u in the carrier of (ExField (x,o)) by ; :: thesis: S1[u,u]
thus S1[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
S1[u,g . u] from 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