let X be RealUnitarySpace; :: thesis: for s1 being sequence of X
for s2 being sequence of (RUSp2RNSp X) st s1 = s2 & s1 is convergent holds
lim s1 = lim s2
let s1 be sequence of X; :: thesis: for s2 being sequence of (RUSp2RNSp X) st s1 = s2 & s1 is convergent holds
lim s1 = lim s2
let s2 be sequence of (RUSp2RNSp X); :: thesis: ( s1 = s2 & s1 is convergent implies lim s1 = lim s2 )
assume AS: s1 = s2 ; :: thesis: ( not s1 is convergent or lim s1 = lim s2 )
assume P1: s1 is convergent ; :: thesis: lim s1 = lim s2
then P5: s2 is convergent by AS, RHS8;
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 lim s2 = lim s1 by P5, NORMSP_1:def 7; :: thesis: verum