consider x being non empty set such that
W: x in X by SETFAM_1:def 11;
reconsider s = NAT --> x as sequence of X by W, FUNCOP_1:57;
take s ; :: thesis: s is non-zero
thus s is non-zero ; :: thesis: verum