take the constant sequence of X ; :: thesis: the constant sequence of X is constant
thus the constant sequence of X is constant ; :: thesis: verum