X in bool X by ZFMISC_1:def 1;
then reconsider IT = NAT --> X as SetSequence of X by FUNCOP_1:57;
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 13;
then IT . n = X by FUNCOP_1:13;
hence IT . n in F by PROB_1:11; :: 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:14;
then X c= union (rng IT) by ZFMISC_1:31;
hence A c= union (rng IT) by XBOOLE_1:1; :: thesis: verum