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

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