let X be NormedLinearTopSpace; :: thesis: for RNS being RealNormSpace
for s being sequence of X
for t being sequence of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & s = t holds
( s is convergent iff t is convergent )
let RNS be RealNormSpace; :: thesis: for s being sequence of X
for t being sequence of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & s = t holds
( s is convergent iff t is convergent )
let s2 be sequence of X; :: thesis: for t being sequence of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & s2 = t holds
( s2 is convergent iff t is convergent )
let t2 be sequence of RNS; :: thesis: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & s2 = t2 implies ( s2 is convergent iff t2 is convergent ) )
assume A1: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & s2 = t2 ) ; :: thesis: ( s2 is convergent iff t2 is convergent )
thus ( s2 is convergent implies t2 is convergent ) by A1, Th26; :: thesis: ( t2 is convergent implies s2 is convergent )
assume A2: t2 is convergent ; :: thesis: s2 is convergent
reconsider y = lim t2 as Point of X by A1;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((s2 . n) - y).|| < r
proof
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((s2 . n) - y).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((s2 . n) - y).|| < r
then consider m being Nat such that
A3: for n being Nat st m <= n holds
||.((t2 . n) - (lim t2)).|| < r by A2, NORMSP_1:def 7;
take m ; :: thesis: for n being Nat st m <= n holds
||.((s2 . n) - y).|| < r
let n be Nat; :: thesis: ( m <= n implies ||.((s2 . n) - y).|| < r )
assume m <= n ; :: thesis: ||.((s2 . n) - y).|| < r
then ||.((t2 . n) - (lim t2)).|| < r by A3;
hence ||.((s2 . n) - y).|| < r by Th19, A1; :: thesis: verum
end;
hence s2 is convergent by Th21; :: thesis: verum