consider x being Element of M;
consider S being sequence of M such that
A1: rng S = {x} by Th10;
take S ; :: thesis: ( S is constant & S is convergent & S is Cauchy & S is bounded )
thus A2: S is constant by A1, FUNCT_2:188; :: 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, TBSP_1:7; :: thesis: S is bounded
thus S is bounded by A2, Th44, TBSP_1:7; :: thesis: verum