let rseq1, rseq2 be convergent Real_Sequence; :: thesis: ( 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; :: thesis: (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; :: thesis: 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 ; :: thesis: 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
let e be Real; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: for n being Nat st n >= N holds
|.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies |.(((ProjMap2 ((addreal * (rseq1,rseq2)),m)) . n) - ((lim rseq1) + (rseq2 . m))).| < e )
assume a4: n >= N ; :: thesis: |.(((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; :: thesis: verum

end;

end;

p1: for m being Element of NAT holds ProjMap2 ((addreal * (rseq1,rseq2)),m) is convergent

proof

let m be Element of NAT ; :: thesis: ProjMap2 ((addreal * (rseq1,rseq2)),m) is convergent
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 by x1;
hence ProjMap2 ((addreal * (rseq1,rseq2)),m) is convergent by SEQ_2:def 6; :: thesis: verum

end;

hence addreal * (rseq1,rseq2) is convergent_in_cod1 ; :: thesis: ( 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 ; :: thesis: 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
let e be Real; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: for n being Nat st n >= N holds
|.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies |.(((ProjMap1 ((addreal * (rseq1,rseq2)),m)) . n) - ((rseq1 . m) + (lim rseq2))).| < e )
assume a4: n >= N ; :: thesis: |.(((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; :: thesis: verum

end;

end;

p2: for m being Element of NAT holds ProjMap1 ((addreal * (rseq1,rseq2)),m) is convergent

proof

let m be Element of NAT ; :: thesis: ProjMap1 ((addreal * (rseq1,rseq2)),m) is convergent
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 by x2;
hence ProjMap1 ((addreal * (rseq1,rseq2)),m) is convergent by SEQ_2:def 6; :: thesis: verum

end;

hence addreal * (rseq1,rseq2) is convergent_in_cod2 ; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: for n being Nat st n >= N holds
|.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies |.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e )
assume n >= N ; :: thesis: |.(((lim_in_cod1 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
then 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; :: thesis: verum

end;

end;

hence lim_in_cod1 (addreal * (rseq1,rseq2)) is convergent by SEQ_2:def 6; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: for n being Nat st n >= N holds
|.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies |.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e )
assume n >= N ; :: thesis: |.(((lim_in_cod2 (addreal * (rseq1,rseq2))) . n) - ((lim rseq1) + (lim rseq2))).| < e
then 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; :: thesis: verum

end;

end;

hence lim_in_cod2 (addreal * (rseq1,rseq2)) is convergent by SEQ_2:def 6; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 :: thesis: verum

proof

let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.(((addreal * (rseq1,rseq2)) . (n,m)) - ((lim rseq1) + (lim rseq2))).| < e )
assume c13: ( n >= N & m >= N ) ; :: thesis: |.(((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; :: thesis: verum

end;

end;

hence addreal * (rseq1,rseq2) is P-convergent ; :: thesis: P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2)
hence P-lim (addreal * (rseq1,rseq2)) = (lim rseq1) + (lim rseq2) by x5, def6; :: thesis: verum