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
proof
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;
then reconsider IT = IT as Set_Sequence of F by Def2;
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