let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: for r being Real st Rseq is P-convergent holds
( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) )
let r be Real; :: thesis: ( Rseq is P-convergent implies ( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) ) )
assume a1: Rseq is P-convergent ; :: thesis: ( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) )
a4: now :: thesis: ( r = 0 implies ( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = 0 ) )
assume a2: r = 0 ; :: thesis: ( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = 0 )
a3: now :: thesis: for n, m being Nat holds (r (#) Rseq) . (n,m) = 0
let n, m be Nat; :: thesis: (r (#) Rseq) . (n,m) = 0
(r (#) Rseq) . (n,m) = r * (Rseq . (n,m)) by VALUED_1:6;
hence (r (#) Rseq) . (n,m) = 0 by a2; :: thesis: verum
end;
hence r (#) Rseq is P-convergent by lm55a; :: thesis: P-lim (r (#) Rseq) = 0
thus P-lim (r (#) Rseq) = 0 by a3, lm55a; :: thesis: verum
end;
now :: thesis: ( r <> 0 implies ( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) ) )
assume r <> 0 ; :: thesis: ( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) )
then a5: |.r.| > 0 by COMPLEX1:47;
a7: now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((r (#) Rseq) . (n,m)) - (r * (P-lim Rseq))).| < e
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((r (#) Rseq) . (n,m)) - (r * (P-lim Rseq))).| < e )
assume 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((r (#) Rseq) . (n,m)) - (r * (P-lim Rseq))).| < e
then consider N being Nat such that
a6: for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (P-lim Rseq)).| < e / |.r.| by a1, a5, def6;
take N = N; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.(((r (#) Rseq) . (n,m)) - (r * (P-lim Rseq))).| < e
hereby :: thesis: verum
let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.(((r (#) Rseq) . (n,m)) - (r * (P-lim Rseq))).| < e )
assume ( n >= N & m >= N ) ; :: thesis: |.(((r (#) Rseq) . (n,m)) - (r * (P-lim Rseq))).| < e
then |.((Rseq . (n,m)) - (P-lim Rseq)).| < e / |.r.| by a6;
then |.r.| * |.((Rseq . (n,m)) - (P-lim Rseq)).| < (e / |.r.|) * |.r.| by a5, XREAL_1:68;
then |.r.| * |.((Rseq . (n,m)) - (P-lim Rseq)).| < |.r.| / (|.r.| / e) by XCMPLX_1:79;
then |.r.| * |.((Rseq . (n,m)) - (P-lim Rseq)).| < e by a5, XCMPLX_1:52;
then |.(r * ((Rseq . (n,m)) - (P-lim Rseq))).| < e by COMPLEX1:65;
then |.((r * (Rseq . (n,m))) - (r * (P-lim Rseq))).| < e ;
hence |.(((r (#) Rseq) . (n,m)) - (r * (P-lim Rseq))).| < e by VALUED_1:6; :: thesis: verum
end;
end;
hence r (#) Rseq is P-convergent ; :: thesis: P-lim (r (#) Rseq) = r * (P-lim Rseq)
hence P-lim (r (#) Rseq) = r * (P-lim Rseq) by a7, def6; :: thesis: verum
end;
hence ( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) ) by a4; :: thesis: verum