let X be set ; :: thesis: for F being Field_Subset of X
for A being Subset of X
for CA being Covering of A,F st A in F holds
ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
let F be Field_Subset of X; :: thesis: for A being Subset of X
for CA being Covering of A,F st A in F holds
ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
let A be Subset of X; :: thesis: for CA being Covering of A,F st A in F holds
ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
let CA be Covering of A,F; :: thesis: ( A in F implies ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) ) )
deffunc H₁( Element of NAT ) -> Element of bool X = ((Partial_Diff_Union CA) . $1) /\ A;
consider FSets being sequence of (bool X) such that
A1: for n being Element of NAT holds FSets . n = H₁(n) from FUNCT_2:sch 4();
reconsider FSets = FSets as SetSequence of X ;
assume A2: A in F ; :: thesis: ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )

now :: thesis: for y being object st y in rng FSets holds
y in F

let y be object ; :: thesis: ( y in rng FSets implies y in F )
assume y in rng FSets ; :: thesis: y in F
then consider x being object such that
A3: x in NAT and
A4: FSets . x = y by FUNCT_2:11;
reconsider n = x as Element of NAT by A3;
A5: FSets . n = ((Partial_Diff_Union CA) . n) /\ A by A1;
Partial_Diff_Union CA is Set_Sequence of F by Th16;
then (Partial_Diff_Union CA) . n in F by Def2;
hence y in F by A2, A4, A5, FINSUB_1:def 2; :: thesis: verum

end;

then rng FSets c= F ;
then reconsider FSets = FSets as sequence of F by FUNCT_2:6;
for m, n being Nat st m <> n holds
FSets . m misses FSets . n

proof

let m, n be Nat; :: thesis: ( m <> n implies FSets . m misses FSets . n )
n in NAT by ORDINAL1:def 12;
then FSets . n = ((Partial_Diff_Union CA) . n) /\ A by A1;
then A6: FSets . n c= (Partial_Diff_Union CA) . n by XBOOLE_1:17;
m in NAT by ORDINAL1:def 12;
then FSets . m = ((Partial_Diff_Union CA) . m) /\ A by A1;
then A7: FSets . m c= (Partial_Diff_Union CA) . m by XBOOLE_1:17;
assume m <> n ; :: thesis: FSets . m misses FSets . n
then (Partial_Diff_Union CA) . m misses (Partial_Diff_Union CA) . n by PROB_3:def 4;
hence FSets . m misses FSets . n by A7, A6, XBOOLE_1:64; :: thesis: verum

end;

then reconsider FSets = FSets as Sep_Sequence of F by PROB_3:def 4;

now :: thesis: for x being object st x in A holds
x in union (rng FSets)

let x be object ; :: thesis: ( x in A implies x in union (rng FSets) )
assume A8: x in A ; :: thesis: x in union (rng FSets)
A c= union (rng CA) by Def3;
then x in union (rng CA) by A8;
then x in Union CA by CARD_3:def 4;
then x in Union (Partial_Diff_Union CA) by PROB_3:20;
then x in union (rng (Partial_Diff_Union CA)) by CARD_3:def 4;
then consider E being set such that
A9: x in E and
A10: E in rng (Partial_Diff_Union CA) by TARSKI:def 4;
consider n being object such that
A11: n in NAT and
A12: (Partial_Diff_Union CA) . n = E by A10, FUNCT_2:11;
reconsider n = n as Element of NAT by A11;
x in ((Partial_Diff_Union CA) . n) /\ A by A8, A9, A12, XBOOLE_0:def 4;
then A13: x in FSets . n by A1;
FSets . n in rng FSets by FUNCT_2:4;
hence x in union (rng FSets) by A13, TARSKI:def 4; :: thesis: verum

end;

then A14: A c= union (rng FSets) ;
take FSets ; :: thesis: ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )

now :: thesis: for x being object st x in union (rng FSets) holds
x in A

let x be object ; :: thesis: ( x in union (rng FSets) implies x in A )
assume x in union (rng FSets) ; :: thesis: x in A
then consider E being set such that
A15: x in E and
A16: E in rng FSets by TARSKI:def 4;
consider n being object such that
A17: n in NAT and
A18: FSets . n = E by A16, FUNCT_2:11;
reconsider n = n as Element of NAT by A17;
x in ((Partial_Diff_Union CA) . n) /\ A by A1, A15, A18;
hence x in A by XBOOLE_0:def 4; :: thesis: verum

end;

then union (rng FSets) c= A ;
hence A = union (rng FSets) by A14, XBOOLE_0:def 10; :: thesis: for n being Nat holds FSets . n c= CA . n

hereby :: thesis: verum

let n be Nat; :: thesis: FSets . n c= CA . n
n in NAT by ORDINAL1:def 12;
then FSets . n = ((Partial_Diff_Union CA) . n) /\ A by A1;
then A19: FSets . n c= (Partial_Diff_Union CA) . n by XBOOLE_1:17;
(Partial_Diff_Union CA) . n c= CA . n by PROB_3:17;
hence FSets . n c= CA . n by A19; :: thesis: verum

end;