let seq be sequence of X; :: thesis: ( seq is constant implies seq is bounded )
assume seq is constant ; :: thesis: seq is bounded
then consider x being Point of X such that
A1: for n being Nat holds seq . n = x by VALUED_0:def 18;
A2: ( x = H1(X) implies seq is bounded )
proof
consider M being Real such that
A3: M > 0 by XREAL_1:1;
reconsider M = M as Real ;
assume A4: x = H1(X) ; :: thesis: seq is bounded
for n being Nat holds ||.(seq . n).|| <= M by A3, A1, A4, BHSP_1:26;
hence seq is bounded by A3; :: thesis: verum
end;
( x <> H1(X) implies seq is bounded )
proof
assume x <> H1(X) ; :: thesis: seq is bounded
consider M being Real such that
A5: ||.x.|| < M by XREAL_1:1;
reconsider M = M as Real ;
( ||.x.|| >= 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) ) by A1, A5, BHSP_1:28;
hence seq is bounded by A5; :: thesis: verum
end;
hence seq is bounded by A2; :: thesis: verum