let rseq1, rseq2 be convergent Real_Sequence; ( addreal * (rseq1,rseq2) is convergent_in_cod1 & addreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (addreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )
set Rseq = addreal * (rseq1,rseq2);
a2:
for n, m being Nat holds (addreal * (rseq1,rseq2)) . (n,m) = (rseq1 . n) + (rseq2 . m)
proof
let n,
m be
Nat;
(addreal * (rseq1,rseq2)) . (n,m) = (rseq1 . n) + (rseq2 . m)
a1:
(
n in NAT &
m in NAT )
by ORDINAL1:def 12;
dom (addreal * (rseq1,rseq2)) = [:NAT,NAT:]
by FUNCT_2:def 1;
then
[n,m] in dom (addreal * (rseq1,rseq2))
by a1, ZFMISC_1:def 2;
then
(addreal * (rseq1,rseq2)) . (
n,
m)
= addreal . (
(rseq1 . n),
(rseq2 . m))
by FINSEQOP:77;
hence
(addreal * (rseq1,rseq2)) . (
n,
m)
= (rseq1 . n) + (rseq2 . m)
by BINOP_2:def 9;
verum
end;
x1:
for m being Element of NAT
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < e
proof
let m be
Element of
NAT ;
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < elet e be
Real;
( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < e )
assume
0 < e
;
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < e
then consider N being
Nat such that a3:
for
n being
Nat st
n >= N holds
|.((rseq1 . n) - (lim rseq1)).| < e
by SEQ_2:def 7;
take
N
;
for n being Nat st n >= N holds
|.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < e
hereby verum
let n be
Nat;
( n >= N implies |.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < e )assume a4:
n >= N
;
|.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < e
n is
Element of
NAT
by ORDINAL1:def 12;
then |.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| =
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (rseq2 . m))).|
by MESFUNC9:def 7
.=
|.(((rseq1 . n) + (rseq2 . m)) - ((lim rseq1) + (rseq2 . m))).|
by a2
.=
|.((rseq1 . n) - (lim rseq1)).|
;
hence
|.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < e
by a3, a4;
verum
end;
end;
p1:
for m being Element of NAT holds ProjMap2 ((addreal * (rseq1,rseq2)),m) is convergent
hence
addreal * (rseq1,rseq2) is convergent_in_cod1
; ( addreal * (rseq1,rseq2) is convergent_in_cod2 & lim_in_cod1 (addreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )
x2:
for m being Element of NAT
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < e
proof
let m be
Element of
NAT ;
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < elet e be
Real;
( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < e )
assume
0 < e
;
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < e
then consider N being
Nat such that a3:
for
n being
Nat st
n >= N holds
|.((rseq2 . n) - (lim rseq2)).| < e
by SEQ_2:def 7;
take
N
;
for n being Nat st n >= N holds
|.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < e
hereby verum
let n be
Nat;
( n >= N implies |.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < e )assume a4:
n >= N
;
|.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < e
n is
Element of
NAT
by ORDINAL1:def 12;
then |.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq2) + (rseq1 . m))).| =
|.(((addreal * (rseq1,rseq2)) . (m,n)) - ((lim rseq2) + (rseq1 . m))).|
by MESFUNC9:def 6
.=
|.(((rseq2 . n) + (rseq1 . m)) - ((lim rseq2) + (rseq1 . m))).|
by a2
.=
|.((rseq2 . n) - (lim rseq2)).|
;
hence
|.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < e
by a3, a4;
verum
end;
end;
p2:
for m being Element of NAT holds ProjMap1 ((addreal * (rseq1,rseq2)),m) is convergent
hence
addreal * (rseq1,rseq2) is convergent_in_cod2
; ( lim_in_cod1 (addreal * (rseq1,rseq2)) is convergent & cod1_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )
x3:
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
proof
let e be
Real;
( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e )
assume
0 < e
;
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
then consider N being
Nat such that a3:
for
n being
Nat st
n >= N holds
|.((rseq2 . n) - (lim rseq2)).| < e
by SEQ_2:def 7;
take
N
;
for n being Nat st n >= N holds
|.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
hereby verum
let n be
Nat;
( n >= N implies |.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e )assume
n >= N
;
|.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < ethen a4:
|.((rseq2 . n) - (lim rseq2)).| < e
by a3;
reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
a5:
ProjMap2 (
(addreal * (rseq1,rseq2)),
n1) is
convergent
by p1;
a6:
(lim_in_cod1 (addreal * (rseq1,rseq2))) . n = lim (ProjMap2 ((addreal * (rseq1,rseq2)),n1))
by def32;
for
e being
Real st
0 < e holds
ex
N being
Nat st
for
m being
Nat st
m >= N holds
|.(((ProjMap2 ((addreal * (rseq1,rseq2)),n1)) . m) - ((lim rseq1) + (rseq2 . n))).| < e
by x1;
then
|.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| = |.(((lim rseq1) + (rseq2 . n)) - ((lim rseq1) + (lim rseq2))).|
by a5, a6, SEQ_2:def 7;
hence
|.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
by a4;
verum
end;
end;
hence
lim_in_cod1 (addreal * (rseq1,rseq2)) is convergent
by SEQ_2:def 6; ( cod1_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )
hence
cod1_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2)
by x3, def34; ( lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )
x4:
for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
proof
let e be
Real;
( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e )
assume
0 < e
;
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
then consider N being
Nat such that a3:
for
n being
Nat st
n >= N holds
|.((rseq1 . n) - (lim rseq1)).| < e
by SEQ_2:def 7;
take
N
;
for n being Nat st n >= N holds
|.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
hereby verum
let n be
Nat;
( n >= N implies |.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e )assume
n >= N
;
|.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < ethen a4:
|.((rseq1 . n) - (lim rseq1)).| < e
by a3;
reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
a5:
ProjMap1 (
(addreal * (rseq1,rseq2)),
n1) is
convergent
by p2;
a6:
(lim_in_cod2 (addreal * (rseq1,rseq2))) . n = lim (ProjMap1 ((addreal * (rseq1,rseq2)),n1))
by def33;
for
e being
Real st
0 < e holds
ex
N being
Nat st
for
m being
Nat st
m >= N holds
|.(((ProjMap1 ((addreal * (rseq1,rseq2)),n1)) . m) - ((rseq1 . n) + (lim rseq2))).| < e
by x2;
then
|.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| = |.(((rseq1 . n) + (lim rseq2)) - ((lim rseq1) + (lim rseq2))).|
by a5, a6, SEQ_2:def 7;
hence
|.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
by a4;
verum
end;
end;
hence
lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent
by SEQ_2:def 6; ( cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) & addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )
hence
cod2_major_iterated_lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2)
by x4, def35; ( addreal * (rseq1,rseq2) is P-convergent & P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) )
x5:
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| < e
proof
let e be
Real;
( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| < e )
assume c1:
0 < e
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| < e
then consider N1 being
Nat such that c4:
for
n being
Nat st
n >= N1 holds
|.((rseq1 . n) - (lim rseq1)).| < e / 2
by SEQ_2:def 7;
consider N2 being
Nat such that c5:
for
n being
Nat st
n >= N2 holds
|.((rseq2 . n) - (lim rseq2)).| < e / 2
by c1, SEQ_2:def 7;
reconsider N =
max (
N1,
N2) as
Nat by TARSKI:1;
take
N
;
for n, m being Nat st n >= N & m >= N holds
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| < e
thus
for
n,
m being
Nat st
n >= N &
m >= N holds
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| < e
verumproof
let n,
m be
Nat;
( n >= N & m >= N implies |.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| < e )
assume c13:
(
n >= N &
m >= N )
;
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| < e
(
max (
N1,
N2)
>= N1 &
max (
N1,
N2)
>= N2 )
by XXREAL_0:25;
then c6:
(
n >= N1 &
m >= N2 )
by c13, XXREAL_0:2;
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| =
|.(((rseq1 . n) + (rseq2 . m)) - ((lim rseq1) + (lim rseq2))).|
by a2
.=
|.(((rseq1 . n) - (lim rseq1)) + ((rseq2 . m) - (lim rseq2))).|
;
then a8:
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| <= |.((rseq1 . n) - (lim rseq1)).| + |.((rseq2 . m) - (lim rseq2)).|
by COMPLEX1:56;
(
|.((rseq1 . n) - (lim rseq1)).| < e / 2 &
|.((rseq2 . m) - (lim rseq2)).| < e / 2 )
by c4, c5, c6;
then
|.((rseq1 . n) - (lim rseq1)).| + |.((rseq2 . m) - (lim rseq2)).| < (e / 2) + (e / 2)
by XREAL_1:8;
hence
|.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| < e
by a8, XXREAL_0:2;
verum
end;
end;
hence
addreal * (rseq1,rseq2) is P-convergent
; P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2)
hence
P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2)
by x5, def6; verum