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_{1}( 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_{1}(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 ) )

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

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

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

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

consider FSets being sequence of (bool X) such that

A1: for n being Element of NAT holds FSets . n = H

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

then
rng FSets c= F
;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;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

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

then reconsider FSets = FSets as Sep_Sequence of F by PROB_3:def 4;
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;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

now :: thesis: for x being object st x in A holds

x in union (rng FSets)

then A14:
A c= union (rng FSets)
;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;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

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

then
union (rng FSets) c= A
;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;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

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