let X be RealUnitarySpace; :: thesis: for seq being sequence of X st X is complete & seq is Cauchy holds
seq is bounded
let seq be sequence of X; :: thesis: ( X is complete & seq is Cauchy implies seq is bounded )
assume that
A1: X is complete and
A2: seq is Cauchy ; :: thesis: seq is bounded
seq is convergent by A1, A2, Def6;
hence seq is bounded by Th24; :: thesis: verum