per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: ex b₁ being sequence of X st b₁ is constant

then reconsider s = {} as sequence of X by FUNCT_2:def 1, RELSET_1:25;
take s ; :: thesis: s is constant
thus s is constant ; :: thesis: verum

end;

suppose X <> {} ; :: thesis: ex b₁ being sequence of X st b₁ is constant

then consider x being set such that
W1: x in X by XBOOLE_0:def 1;
reconsider s = NAT --> x as sequence of X by W1, FUNCOP_1:57;
take s ; :: thesis: s is constant
thus s is constant ; :: thesis: verum

end;

end;