let X be set ; :: thesis:
let F be Field_Subset of X; :: thesis:
let A be Subset of X; :: thesis:
let CA be Covering of A,F; :: thesis:
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:

now :: thesis:

let y be object ; :: thesis:
assume y in rng FSets ; :: thesis:
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:

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:
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:
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:

end;

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

now :: thesis:

let x be object ; :: thesis:
assume A8: x in A ; :: thesis:
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:

end;

then A14: A c= union (rng FSets) ;
take FSets ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in union (rng FSets) ; :: thesis:
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:

end;

then union (rng FSets) c= A ;
hence A = union (rng FSets) by A14, XBOOLE_0:def 10; :: thesis:

hereby :: thesis:

let n be Nat; :: thesis:
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:

end;