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 Function of NAT,(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

let y be set ; :: thesis: ( y in rng FSets implies y in F )
assume y in rng FSets ; :: thesis: y in F
then consider x being set 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 by TARSKI:def 3;
then reconsider FSets = FSets as Function of NAT,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 A7: 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 A8: 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 A8, A7, XBOOLE_1:64; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in A implies x in union (rng FSets) )
assume A9: x in A ; :: thesis: x in union (rng FSets)
A c= union (rng CA) by Def3;
then x in union (rng CA) by A9;
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
A10: x in E and
A11: E in rng (Partial_Diff_Union CA) by TARSKI:def 4;
consider n being set such that
A12: n in NAT and
A13: (Partial_Diff_Union CA) . n = E by A11, FUNCT_2:11;
reconsider n = n as Element of NAT by A12;
x in ((Partial_Diff_Union CA) . n) /\ A by A9, A10, A13, XBOOLE_0:def 4;
then A14: x in FSets . n by A1;
FSets . n in rng FSets by FUNCT_2:4;
hence x in union (rng FSets) by A14, TARSKI:def 4; :: thesis: verum

end;

then A15: A c= union (rng FSets) by TARSKI:def 3;
take FSets ; :: thesis: ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )

now

let x be set ; :: 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
A16: x in E and
A17: E in rng FSets by TARSKI:def 4;
consider n being set such that
A18: n in NAT and
A19: FSets . n = E by A17, FUNCT_2:11;
reconsider n = n as Element of NAT by A18;
x in ((Partial_Diff_Union CA) . n) /\ A by A1, A16, A19;
hence x in A by XBOOLE_0:def 4; :: thesis: verum

end;

then union (rng FSets) c= A by TARSKI:def 3;
hence A = union (rng FSets) by A15, 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 A20: 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 A20, XBOOLE_1:1; :: thesis: verum

end;