per cases ( X = {} or X <> {} ) ;
suppose X = {} ; :: thesis: ex b1 being sequence of X st b1 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 b1 being sequence of X st b1 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;