set x = the Element of M;
consider S being sequence of M such that
A1: rng S = { the Element of M} by Th7;
take S ; :: thesis: ( S is constant & S is convergent & S is Cauchy & S is bounded )
thus A2: S is constant by A1, FUNCT_2:111; :: thesis: ( S is convergent & S is Cauchy & S is bounded )
hence S is convergent ; :: thesis: ( S is Cauchy & S is bounded )
thus S is Cauchy by A2; :: thesis: S is bounded
thus S is bounded by A2; :: thesis: verum