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