let s1 be sequence of V; :: thesis:
assume A2: ( rng s1 c= CV1 & s1 is convergent ) ; :: thesis:
then reconsider s2 = s1 as sequence of V1 by A1, FUNCT_2:6;
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.((s2 . m) - (s2 . n)).|| < s

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider n being Nat such that
A3: for m being Nat st n <= m holds
||.((s1 . m) - (s1 . n)).|| < s by A2, LOPBAN_3:4;
take n ; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then A4: ||.((s1 . m) - (s1 . n)).|| < s by A3;
- (s1 . n) = (- 1) * (s1 . n) by RLVECT_1:16
.= (- 1) * (s2 . n) by SUBTH0
.= - (s2 . n) by RLVECT_1:16 ;
then (s1 . m) - (s1 . n) = (s2 . m) - (s2 . n) by SUBTH0;
hence ||.((s2 . m) - (s2 . n)).|| < s by A4, SUBTH0; :: thesis:

end;

then A6: s2 is convergent by A1, LOPBAN_1:def 15, LOPBAN_3:5;
the carrier of V1 c= the carrier of V by DUALSP01:def 16;
then reconsider s0 = lim s2 as Point of V ;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((s1 . n) - s0).|| < r

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider m being Nat such that
A7: for n being Nat st m <= n holds
||.((s2 . n) - (lim s2)).|| < r by A6, NORMSP_1:def 7;
take m ; :: thesis:
let n be Nat; :: thesis:
assume m <= n ; :: thesis:
then A8: ||.((s2 . n) - (lim s2)).|| < r by A7;
- (lim s2) = (- 1) * (lim s2) by RLVECT_1:16
.= (- 1) * s0 by SUBTH0
.= - s0 by RLVECT_1:16 ;
then (s2 . n) - (lim s2) = (s1 . n) - s0 by SUBTH0;
hence ||.((s1 . n) - s0).|| < r by A8, SUBTH0; :: thesis:

end;

end;