let X be RealUnitarySpace; :: thesis: for s1 being sequence of X
for s2 being sequence of (RUSp2RNSp X) st s1 = s2 holds
( s1 is convergent iff s2 is convergent )
let s1 be sequence of X; :: thesis: for s2 being sequence of (RUSp2RNSp X) st s1 = s2 holds
( s1 is convergent iff s2 is convergent )
let s2 be sequence of (RUSp2RNSp X); :: thesis: ( s1 = s2 implies ( s1 is convergent iff s2 is convergent ) )
assume AS: s1 = s2 ; :: thesis: ( s1 is convergent iff s2 is convergent )

hereby :: thesis: ( s2 is convergent implies s1 is convergent )

assume P1: s1 is convergent ; :: thesis: s2 is convergent
reconsider g1 = lim s1 as Point of (RUSp2RNSp X) ;

now :: thesis: for p being Real st 0 < p holds
ex m being Nat st
for n being Nat st m <= n holds
||.((s2 . n) - g1).|| < p

let p be Real; :: thesis: ( 0 < p implies ex m being Nat st
for n being Nat st m <= n holds
||.((s2 . n) - g1).|| < p )
assume 0 < p ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((s2 . n) - g1).|| < p
then consider m being Nat such that
P2: for n being Nat st m <= n holds
||.((s1 . n) - (lim s1)).|| < p by P1, BHSP_2:19;
take m = m; :: thesis: for n being Nat st m <= n holds
||.((s2 . n) - g1).|| < p
thus for n being Nat st m <= n holds
||.((s2 . n) - g1).|| < p :: thesis: verum

proof

let n be Nat; :: thesis: ( m <= n implies ||.((s2 . n) - g1).|| < p )
assume m <= n ; :: thesis: ||.((s2 . n) - g1).|| < p
then P3: ||.((s1 . n) - (lim s1)).|| < p by P2;
(s1 . n) - (lim s1) = (s2 . n) - g1 by AS, RHS3;
hence ||.((s2 . n) - g1).|| < p by P3, Def1; :: thesis: verum

end;

end;

hence s2 is convergent ; :: thesis: verum

end;

assume P4: s2 is convergent ; :: thesis: s1 is convergent
reconsider g2 = lim s2 as Point of X ;

now :: thesis: for p being Real st 0 < p holds
ex m being Nat st
for n being Nat st m <= n holds
||.((s1 . n) - g2).|| < p

let p be Real; :: thesis: ( 0 < p implies ex m being Nat st
for n being Nat st m <= n holds
||.((s1 . n) - g2).|| < p )
assume 0 < p ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((s1 . n) - g2).|| < p
then consider m being Nat such that
P2: for n being Nat st m <= n holds
||.((s2 . n) - (lim s2)).|| < p by P4, NORMSP_1:def 7;
take m = m; :: thesis: for n being Nat st m <= n holds
||.((s1 . n) - g2).|| < p
thus for n being Nat st m <= n holds
||.((s1 . n) - g2).|| < p :: thesis: verum

proof

let n be Nat; :: thesis: ( m <= n implies ||.((s1 . n) - g2).|| < p )
assume m <= n ; :: thesis: ||.((s1 . n) - g2).|| < p
then P3: ||.((s2 . n) - (lim s2)).|| < p by P2;
(s2 . n) - (lim s2) = (s1 . n) - g2 by AS, RHS3;
hence ||.((s1 . n) - g2).|| < p by P3, Def1; :: thesis: verum

end;

end;

hence s1 is convergent by BHSP_2:9; :: thesis: verum