let X be RealUnitarySpace; :: thesis: for seq being sequence of X st seq is V8() holds
seq is bounded
let seq be sequence of X; :: thesis: ( seq is V8() implies seq is bounded )
assume seq is V8() ; :: 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 = H₁(X) implies seq is bounded )

proof

consider M being real number such that
A3: M > 0 by XREAL_1:3;
reconsider M = M as Real by XREAL_0:def 1;
assume A4: x = H₁(X) ; :: thesis: seq is bounded

now

let n be Element of NAT ; :: thesis: ||.(seq . n).|| <= M
seq . n = H₁(X) by A1, A4;
hence ||.(seq . n).|| <= M by A3, BHSP_1:32; :: thesis: verum

end;

hence seq is bounded by A3, Def3; :: thesis: verum

end;

( x <> H₁(X) implies seq is bounded )

proof

assume x <> H₁(X) ; :: thesis: seq is bounded
consider M being real number such that
A5: ||.x.|| < M by XREAL_1:3;
reconsider M = M as Real by XREAL_0:def 1;
( ||.x.|| >= 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) ) by A1, A5, BHSP_1:34;
hence seq is bounded by A5, Def3; :: thesis: verum

end;

hence seq is bounded by A2; :: thesis: verum