set K = unionField (S,f,E);
H: the carrier of (unionField (S,f,E)) = unionCarrier (S,f,E) by duf
.= union { the carrier of (p `1) where p is Element of S : verum } ;
defpred S<sub>1</sub>[ object , object ] means ex p being Element of S st
( $1 is Element of (p `1) & $2 = (p `2) . $1 );

A: now :: thesis: for x being object st x in the carrier of (unionField (S,f,E)) holds
ex y being object st
( y in the carrier of L & S₁[x,y] )

let x be object ; :: thesis: ( x in the carrier of (unionField (S,f,E)) implies ex y being object st
( y in the carrier of L & S₁[x,y] ) )
assume x in the carrier of (unionField (S,f,E)) ; :: thesis: ex y being object st
( y in the carrier of L & S₁[x,y] )
then consider Y being set such that
A1: ( x in Y & Y in { the carrier of (p `1) where p is Element of S : verum } ) by H, TARSKI:def 4;
consider p being Element of S such that
A2: Y = the carrier of (p `1) by A1;
reconsider a = x as Element of (p `1) by A1, A2;
thus ex y being object st
( y in the carrier of L & S₁[x,y] ) :: thesis: verum

proof

take b = (p `2) . a; :: thesis: ( b in the carrier of L & S₁[x,b] )
thus ( b in the carrier of L & S₁[x,b] ) ; :: thesis: verum

end;

end;

consider g being Function of the carrier of (unionField (S,f,E)), the carrier of L such that
B: for x being object st x in the carrier of (unionField (S,f,E)) holds
S₁[x,g . x] from FUNCT_2:sch 1(A);
take g ; :: thesis: for p being Element of S holds g | the carrier of (p `1) = p `2

now :: thesis: for p being Element of S holds g | the carrier of (p `1) = p `2

let p be Element of S; :: thesis: g | the carrier of (p `1) = p `2
p `1 is Subfield of unionField (S,f,E) by Fsubb;
then I: the carrier of (p `1) c= the carrier of (unionField (S,f,E)) by EC_PF_1:def 1;
B0: (dom g) /\ the carrier of (p `1) = the carrier of (unionField (S,f,E)) /\ the carrier of (p `1) by FUNCT_2:def 1
.= the carrier of (p `1) by I, XBOOLE_1:28
.= dom (p `2) by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom (p `2) holds
(p `2) . o = g . o

let o be object ; :: thesis: ( o in dom (p `2) implies (p `2) . b₁ = g . b₁ )
assume J: o in dom (p `2) ; :: thesis: (p `2) . b₁ = g . b₁
then consider q being Element of S such that
B1: ( o is Element of (q `1) & g . o = (q `2) . o ) by B, I;

per cases ( p <= q or q <= p ) by dasc;

suppose p <= q ; :: thesis: (p `2) . b₁ = g . b₁

hence (p `2) . o = g . o by B1, J, FIELD_8:def 6; :: thesis: verum

end;

suppose q <= p ; :: thesis: (p `2) . b₁ = g . b₁

hence (p `2) . o = g . o by B1, FIELD_8:def 6; :: thesis: verum

end;

end;

end;

hence g | the carrier of (p `1) = p `2 by B0, FUNCT_1:46; :: thesis: verum

end;

hence for p being Element of S holds g | the carrier of (p `1) = p `2 ; :: thesis: verum