let r be Real; :: thesis: ( 0 < r implies ex k being Nat st
for n being Nat st k <= n holds
|.((||.(S - g).|| . n) - 0).| < r )
assume A4: 0 < r ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
|.((||.(S - g).|| . n) - 0).| < r
consider m1 being Nat such that
A5: for n being Nat st m1 <= n holds
||.((S . n) - g).|| < r by A1, A2, A4, Def7;
reconsider k = m1 as Nat ;
take k = k; :: thesis: for n being Nat st k <= n holds
|.((||.(S - g).|| . n) - 0).| < r
let n be Nat; :: thesis: ( k <= n implies |.((||.(S - g).|| . n) - 0).| < r )
assume A6: k <= n ; :: thesis: |.((||.(S - g).|| . n) - 0).| < r
reconsider nn = n as Nat ;
||.((S . nn) - g).|| < r by A5, A6;
then A7: ||.(((S . nn) - g) - H₁(RNS)).|| < r ;
|.(||.((S . nn) - g).|| - ||.H₁(RNS).||).| <= ||.(((S . nn) - g) - H₁(RNS)).|| by Th9;
then |.(||.((S . nn) - g).|| - ||.H₁(RNS).||).| < r by A7, XXREAL_0:2;
then |.(||.((S - g) . nn).|| - 0).| < r by Def4;
hence |.((||.(S - g).|| . n) - 0).| < r by NORMSP_0:def 4; :: thesis: verum