X in bool X by ZFMISC_1:def 1;
then reconsider A = NAT --> X as SetSequence of X by FUNCOP_1:57;
take A ; :: thesis: for n being Nat holds A . n in F
let n be Nat; :: thesis: A . n in F
n is Element of NAT by ORDINAL1:def 13;
then A . n = X by FUNCOP_1:13;
hence A . n in F by PROB_1:11; :: thesis: verum