let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
||.((S . m) - g).|| < r )
reconsider p = r as Real ;
assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((S . m) - g).|| < r
then consider n being Nat such that
A3: for m being Nat st n <= m holds
|.((||.(S - g).|| . m) - 0).| < p by A1, SEQ_2:def 7;
reconsider n = n as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
||.((S . m) - g).|| < r
let m be Nat; :: thesis: ( n <= m implies ||.((S . m) - g).|| < r )
assume n <= m ; :: thesis: ||.((S . m) - g).|| < r
then |.((||.(S - g).|| . m) - 0).| < p by A3;
then |.||.((S - g) . m).||.| < p by NORMSP_0:def 4;
then |.||.((S . m) - g).||.| < p by NORMSP_1:def 4;
hence ||.((S . m) - g).|| < r by ABSVALUE:def 1, NORMSP_1:4; :: thesis: verum