let S, T be RealNormSpace; for R being RestFunc of S,T
for s being 0. S -convergent sequence of S st s is non-zero holds
( R /* s is convergent & lim (R /* s) = 0. T )
let R be RestFunc of S,T; for s being 0. S -convergent sequence of S st s is non-zero holds
( R /* s is convergent & lim (R /* s) = 0. T )
let s be 0. S -convergent sequence of S; ( s is non-zero implies ( R /* s is convergent & lim (R /* s) = 0. T ) )
assume A1:
s is non-zero
; ( R /* s is convergent & lim (R /* s) = 0. T )
A2:
(||.s.|| ") (#) (R /* s) is convergent
by Def5, A1;
then A4:
||.s.|| (#) ((||.s.|| ") (#) (R /* s)) = R /* s
by FUNCT_2:63;
A5:
s is convergent
by Def4;
then A6:
||.s.|| is convergent
by LOPBAN_1:41;
lim s = 0. S
by Def4;
then
lim ||.s.|| = ||.(0. S).||
by A5, LOPBAN_1:41;
then A7:
lim ||.s.|| = 0
by NORMSP_1:1;
lim ((||.s.|| ") (#) (R /* s)) = 0. T
by Def5, A1;
then
lim (R /* s) = 0 * (0. T)
by A5, A4, A2, A7, Th14, LOPBAN_1:41;
hence
( R /* s is convergent & lim (R /* s) = 0. T )
by A4, A2, A6, Th13, RLVECT_1:10; verum