let RNS be RealNormSpace; :: thesis: for S being sequence of RNS st S is convergent holds
||.S.|| is convergent
let S be sequence of RNS; :: thesis: ( S is convergent implies ||.S.|| is convergent )
assume S is convergent ; :: thesis: ||.S.|| is convergent
then consider g being Point of RNS such that
A1: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - g).|| < r ;
now :: thesis: for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
|.((||.S.|| . n) - ||.g.||).| < r
let r be Real; :: thesis: ( 0 < r implies ex k being Nat st
for n being Nat st k <= n holds
|.((||.S.|| . n) - ||.g.||).| < r )
assume A2: 0 < r ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
|.((||.S.|| . n) - ||.g.||).| < r
consider m1 being Nat such that
A3: for n being Nat st m1 <= n holds
||.((S . n) - g).|| < r by A1, A2;
reconsider k = m1 as Nat ;
take k = k; :: thesis: for n being Nat st k <= n holds
|.((||.S.|| . n) - ||.g.||).| < r
now :: thesis: for n being Nat st k <= n holds
|.((||.S.|| . n) - ||.g.||).| < r
let n be Nat; :: thesis: ( k <= n implies |.((||.S.|| . n) - ||.g.||).| < r )
assume A4: k <= n ; :: thesis: |.((||.S.|| . n) - ||.g.||).| < r
reconsider nn = n as Nat ;
A5: ||.((S . nn) - g).|| < r by A3, A4;
|.(||.(S . nn).|| - ||.g.||).| <= ||.((S . nn) - g).|| by Th9;
then |.(||.(S . nn).|| - ||.g.||).| < r by A5, XXREAL_0:2;
hence |.((||.S.|| . n) - ||.g.||).| < r by NORMSP_0:def 4; :: thesis: verum
end;
hence for n being Nat st k <= n holds
|.((||.S.|| . n) - ||.g.||).| < r ; :: thesis: verum
end;
hence ||.S.|| is convergent by SEQ_2:def 6; :: thesis: verum