let a be Real; :: thesis: for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
a * S is convergent
let RNS be RealNormSpace; :: thesis: for S being sequence of RNS st S is convergent holds
a * S is convergent
let S be sequence of RNS; :: thesis: ( S is convergent implies a * S is convergent )
assume S is convergent ; :: thesis: a * S is convergent
then consider g being Point of RNS such that
A1: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - g).|| < r ;
take h = a * g; :: according to NORMSP_1:def 6 :: thesis: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.(((a * S) . n) - h).|| < r
A2: now :: thesis: ( a <> 0 implies for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r )
assume A3: a <> 0 ; :: thesis: for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r
then A4: 0 < |.a.| by COMPLEX1:47;
let r be Real; :: thesis: ( 0 < r implies ex k being Nat st
for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r )
assume 0 < r ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r
then consider m1 being Nat such that
A5: for n being Nat st m1 <= n holds
||.((S . n) - g).|| < r / |.a.| by A1, A4;
take k = m1; :: thesis: for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r
let n be Nat; :: thesis: ( k <= n implies ||.(((a * S) . n) - h).|| < r )
assume k <= n ; :: thesis: ||.(((a * S) . n) - h).|| < r
then A6: ||.((S . n) - g).|| < r / |.a.| by A5;
A7: 0 <> |.a.| by A3, COMPLEX1:47;
A8: |.a.| * (r / |.a.|) = |.a.| * ((|.a.| ") * r) by XCMPLX_0:def 9
.= (|.a.| * (|.a.| ")) * r
.= 1 * r by A7, XCMPLX_0:def 7
.= r ;
||.((a * (S . n)) - (a * g)).|| = ||.(a * ((S . n) - g)).|| by RLVECT_1:34
.= |.a.| * ||.((S . n) - g).|| by Def1 ;
then ||.((a * (S . n)) - h).|| < r by A4, A6, A8, XREAL_1:68;
hence ||.(((a * S) . n) - h).|| < r by Def5; :: thesis: verum
end;
now :: thesis: ( a = 0 implies for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r )
assume A9: a = 0 ; :: thesis: for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r
let r be Real; :: thesis: ( 0 < r implies ex k being Nat st
for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r )
assume 0 < r ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r
then consider m1 being Nat such that
A10: for n being Nat st m1 <= n holds
||.((S . n) - g).|| < r by A1;
take k = m1; :: thesis: for n being Nat st k <= n holds
||.(((a * S) . n) - h).|| < r
let n be Nat; :: thesis: ( k <= n implies ||.(((a * S) . n) - h).|| < r )
assume k <= n ; :: thesis: ||.(((a * S) . n) - h).|| < r
then A11: ||.((S . n) - g).|| < r by A10;
||.((a * (S . n)) - (a * g)).|| = ||.((0 * (S . n)) - H1(RNS)).|| by A9, RLVECT_1:10
.= ||.(H1(RNS) - H1(RNS)).|| by RLVECT_1:10
.= ||.H1(RNS).||
.= 0 ;
then ||.((a * (S . n)) - h).|| < r by A11;
hence ||.(((a * S) . n) - h).|| < r by Def5; :: thesis: verum
end;
hence for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.(((a * S) . n) - h).|| < r by A2; :: thesis: verum