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