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:12;
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 object such that
A1: x in X by XBOOLE_0:def 1;
reconsider s = NAT --> x as sequence of X by A1, FUNCOP_1:45;
take s ; :: thesis: s is constant
thus s is constant ; :: thesis: verum

end;

end;