X in bool X by ZFMISC_1:def 1;
then reconsider A = NAT --> X as SetSequence of X by FUNCOP_1:45;
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 12;
then A . n = X by FUNCOP_1:7;
hence A . n in F by PROB_1:5; :: thesis: verum