let X be set ; :: thesis: for F being Field_Subset of X

for A being Subset of X st A in F holds

(A,({} X)) followed_by ({} X) is Covering of A,F

let F be Field_Subset of X; :: thesis: for A being Subset of X st A in F holds

(A,({} X)) followed_by ({} X) is Covering of A,F

let A be Subset of X; :: thesis: ( A in F implies (A,({} X)) followed_by ({} X) is Covering of A,F )

reconsider Sets = (A,({} X)) followed_by ({} X) as SetSequence of X ;

A1: Sets . 0 = A by FUNCT_7:122;

A2: Sets . 1 = {} X by FUNCT_7:123;

assume A3: A in F ; :: thesis: (A,({} X)) followed_by ({} X) is Covering of A,F

for n being Nat holds Sets . n in F

A c= union (rng Sets)

for A being Subset of X st A in F holds

(A,({} X)) followed_by ({} X) is Covering of A,F

let F be Field_Subset of X; :: thesis: for A being Subset of X st A in F holds

(A,({} X)) followed_by ({} X) is Covering of A,F

let A be Subset of X; :: thesis: ( A in F implies (A,({} X)) followed_by ({} X) is Covering of A,F )

reconsider Sets = (A,({} X)) followed_by ({} X) as SetSequence of X ;

A1: Sets . 0 = A by FUNCT_7:122;

A2: Sets . 1 = {} X by FUNCT_7:123;

assume A3: A in F ; :: thesis: (A,({} X)) followed_by ({} X) is Covering of A,F

for n being Nat holds Sets . n in F

proof

then reconsider Sets = Sets as Set_Sequence of F by Def2;
let n be Nat; :: thesis: Sets . n in F

end;A c= union (rng Sets)

proof

hence
(A,({} X)) followed_by ({} X) is Covering of A,F
by Def3; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in union (rng Sets) )

dom Sets = NAT by FUNCT_2:def 1;

then A4: Sets . 0 in rng Sets by FUNCT_1:3;

assume x in A ; :: thesis: x in union (rng Sets)

hence x in union (rng Sets) by A1, A4, TARSKI:def 4; :: thesis: verum

end;dom Sets = NAT by FUNCT_2:def 1;

then A4: Sets . 0 in rng Sets by FUNCT_1:3;

assume x in A ; :: thesis: x in union (rng Sets)

hence x in union (rng Sets) by A1, A4, TARSKI:def 4; :: thesis: verum