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] )
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 FUNCT_2:sch 1(A2);
reconsider g = g as Function of F,(ExField (x,o)) ;
take
g
; ( 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; verum