X in bool X
by ZFMISC_1:def 1;

then reconsider IT = NAT --> X as SetSequence of X by FUNCOP_1:45;

for n being Nat holds IT . n in F

take IT ; :: thesis: A c= union (rng IT)

rng IT = {X} by FUNCOP_1:8;

then X c= union (rng IT) by ZFMISC_1:25;

hence A c= union (rng IT) ; :: thesis: verum

then reconsider IT = NAT --> X as SetSequence of X by FUNCOP_1:45;

for n being Nat holds IT . n in F

proof

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

n in NAT by ORDINAL1:def 12;

then IT . n = X by FUNCOP_1:7;

hence IT . n in F by PROB_1:5; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

then IT . n = X by FUNCOP_1:7;

hence IT . n in F by PROB_1:5; :: thesis: verum

take IT ; :: thesis: A c= union (rng IT)

rng IT = {X} by FUNCOP_1:8;

then X c= union (rng IT) by ZFMISC_1:25;

hence A c= union (rng IT) ; :: thesis: verum