let J, K, L be ExtREAL_sequence; :: thesis: ( ( for n, m being Nat st n <= m holds
J . n <= J . m ) & ( for n, m being Nat st n <= m holds
K . n <= K . m ) & J is () & K is () & ( for n being Nat holds (J . n) + (K . n) = L . n ) implies ( L is convergent & lim L = sup (rng L) & lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) ) )
assume that
A1: for n, m being Nat st n <= m holds
J . n <= J . m and
A2: for n, m being Nat st n <= m holds
K . n <= K . m and
A3: J is () and
A4: K is () and
A5: for n being Nat holds (J . n) + (K . n) = L . n ; :: thesis: ( L is convergent & lim L = sup (rng L) & lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )
A6: dom K = NAT by FUNCT_2:def 1;
A7: dom J = NAT by FUNCT_2:def 1;

A8: now :: thesis: ( L is convergent & lim L = (sup (rng J)) + (sup (rng K)) )

per cases ( sup (rng J) in REAL or sup (rng J) = +infty ) by A3, Lm8;

suppose A9: sup (rng J) in REAL ; :: thesis: ( L is convergent & lim L = (sup (rng J)) + (sup (rng K)) )

then reconsider SJ = sup (rng J) as Real ;

per cases ( sup (rng K) in REAL or sup (rng K) = +infty ) by A4, Lm8;

suppose A10: sup (rng K) in REAL ; :: thesis: ( L is convergent & lim L = (sup (rng J)) + (sup (rng K)) )

then reconsider SK = sup (rng K) as Real ;

A11: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (SJ + SK)).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (SJ + SK)).| < p )
assume A12: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (SJ + SK)).| < p
then consider SJ9 being ExtReal such that
A13: SJ9 in rng J and
A14: (sup (rng J)) - (p / 2) < SJ9 by A9, MEASURE6:6;
consider nj being object such that
A15: nj in dom J and
A16: SJ9 = J . nj by A13, FUNCT_1:def 3;
reconsider nj = nj as Element of NAT by A15;
consider SK9 being ExtReal such that
A17: SK9 in rng K and
A18: (sup (rng K)) - (p / 2) < SK9 by A10, A12, MEASURE6:6;
consider nk being object such that
A19: nk in dom K and
A20: SK9 = K . nk by A17, FUNCT_1:def 3;
reconsider nk = nk as Element of NAT by A19;
reconsider n = max (nj,nk) as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((L . m) - (SJ + SK)).| < p

hereby :: thesis: verum

reconsider SJ9 = SJ9, SK9 = SK9 as R_eal by XXREAL_0:def 1;
let m be Nat; :: thesis: ( n <= m implies |.((L . m) - (SJ + SK)).| < p )
assume A21: n <= m ; :: thesis: |.((L . m) - (SJ + SK)).| < p
nk <= n by XXREAL_0:25;
then nk <= m by A21, XXREAL_0:2;
then SK9 <= K . m by A2, A20;
then A22: SK - (K . m) <= SK - SK9 by XXREAL_3:37;
nj <= n by XXREAL_0:25;
then nj <= m by A21, XXREAL_0:2;
then SJ9 <= J . m by A1, A16;
then SJ - (J . m) <= SJ - SJ9 by XXREAL_3:37;
then A23: (SJ - (J . m)) + (SK - (K . m)) <= (SJ - SJ9) + (SK - SK9) by A22, XXREAL_3:36;
SJ in REAL by XREAL_0:def 1;
then A24: SJ < +infty by XXREAL_0:9;
reconsider s1 = SK as Element of REAL by XREAL_0:def 1;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
A25: - ((L . m) - (SJ + SK)) = (SJ + SK) - (L . m) by XXREAL_3:26;
A26: p / 2 in REAL by XREAL_0:def 1;
SK < (p / 2) + SK9 by A18, XXREAL_3:54;
then SK - SK9 < p / 2 by XXREAL_3:55;
then A27: (p / 2) + (SK - SK9) < (p / 2) + (p / 2) by XXREAL_3:43, A26;
SJ < (p / 2) + SJ9 by A14, XXREAL_3:54;
then A28: SJ - SJ9 < p / 2 by XXREAL_3:55;
nk <= n by XXREAL_0:25;
then nk <= m by A21, XXREAL_0:2;
then A29: K . nk <= K . m by A2;
A30: SK in REAL by XREAL_0:def 1;
then A31: SK < +infty by XXREAL_0:9;
K . m1 in rng K by A6, FUNCT_1:3;
then A32: K . m <= SK by XXREAL_2:4;
then A33: K . m < +infty by A30, XXREAL_0:2, XXREAL_0:9;
-infty < SK9 by A4, A20;
then reconsider s0 = SK9 as Element of REAL by A20, A33, A29, XXREAL_0:14;
A34: L . m = (J . m) + (K . m) by A5;
J . m1 in rng J by A7, FUNCT_1:3;
then A35: J . m <= SJ by XXREAL_2:4;
then (J . m) + (K . m) <= SJ + SK by A32, XXREAL_3:36;
then (L . m) - (SJ + SK) <= 0 by A34, A25, XXREAL_3:40;
then A36: |.((L . m) - (SJ + SK)).| = (SJ + SK) - (L . m) by A25, EXTREAL1:18;
SK - SK9 = s1 - s0 by SUPINF_2:3;
then (SJ - SJ9) + (SK - SK9) < (p / 2) + (SK - SK9) by A28, XXREAL_3:43;
then A37: (SJ - SJ9) + (SK - SK9) < (p / 2) + (p / 2) by A27, XXREAL_0:2;
-infty < K . m by A4;
then (SJ - (J . m)) + (SK - (K . m)) = ((SJ - (J . m)) + SK) - (K . m) by A33, XXREAL_3:30
.= ((SK + SJ) - (J . m)) - (K . m) by XXREAL_3:30
.= (SK + SJ) - ((J . m) + (K . m)) by A24, A31, A35, A32, XXREAL_3:31
.= (SK + SJ) - (L . m) by A5 ;
hence |.((L . m) - (SJ + SK)).| < p by A36, A37, A23, XXREAL_0:2; :: thesis: verum

end;

end;

then A38: L is convergent_to_finite_number ;
hence L is convergent ; :: thesis: lim L = (sup (rng J)) + (sup (rng K))
hence lim L = (sup (rng J)) + (sup (rng K)) by A11, A38, Def12; :: thesis: verum

end;

suppose A39: sup (rng K) = +infty ; :: thesis: ( L is convergent & lim L = (sup (rng J)) + (sup (rng K)) )

for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
p <= L . m

proof

reconsider supj = sup (rng J) as Element of REAL by A9;
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
p <= L . m )
reconsider p92 = p / 2, p9 = p as Element of REAL by XREAL_0:def 1;
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
p <= L . m
then consider j being ExtReal such that
A40: j in rng J and
A41: (sup (rng J)) - (p / 2) < j by A9, MEASURE6:6;
consider n1 being object such that
A42: n1 in dom J and
A43: j = J . n1 by A40, FUNCT_1:def 3;
A44: supj - p92 = (sup (rng J)) - (p / 2) by SUPINF_2:3;
then A45: p9 - (supj - p92) = p - ((sup (rng J)) - (p / 2)) by SUPINF_2:3;
then p - ((sup (rng J)) - (p / 2)) < sup (rng K) by A39, XXREAL_0:9;
then consider k being Element of ExtREAL such that
A46: k in rng K and
A47: p - ((sup (rng J)) - (p / 2)) < k by XXREAL_2:94;
p9 = (p9 - (supj - p92)) + (supj - p92) ;
then A48: (p - ((sup (rng J)) - (p / 2))) + ((sup (rng J)) - (p / 2)) = p9 by A44, A45, SUPINF_2:1;
reconsider n1 = n1 as Element of NAT by A42;
consider n2 being object such that
A49: n2 in dom K and
A50: k = K . n2 by A46, FUNCT_1:def 3;
reconsider n2 = n2 as Element of NAT by A49;
set n = max (n1,n2);
J . n1 <= J . (max (n1,n2)) by A1, XXREAL_0:25;
then A51: (sup (rng J)) - (p / 2) < J . (max (n1,n2)) by A41, A43, XXREAL_0:2;
K . n2 <= K . (max (n1,n2)) by A2, XXREAL_0:25;
then A52: p - ((sup (rng J)) - (p / 2)) < K . (max (n1,n2)) by A47, A50, XXREAL_0:2;
A53: p < (J . (max (n1,n2))) + (K . (max (n1,n2))) by A51, A52, A48, XXREAL_3:64;

now :: thesis: for m being Nat st max (n1,n2) <= m holds
p <= L . m

let m be Nat; :: thesis: ( max (n1,n2) <= m implies p <= L . m )
assume A54: max (n1,n2) <= m ; :: thesis: p <= L . m
then A55: K . (max (n1,n2)) <= K . m by A2;
J . (max (n1,n2)) <= J . m by A1, A54;
then (J . (max (n1,n2))) + (K . (max (n1,n2))) <= (J . m) + (K . m) by A55, XXREAL_3:36;
then (J . (max (n1,n2))) + (K . (max (n1,n2))) <= L . m by A5;
hence p <= L . m by A53, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
p <= L . m ; :: thesis: verum

end;

then A56: L is convergent_to_+infty ;
hence L is convergent ; :: thesis: lim L = (sup (rng J)) + (sup (rng K))
then lim L = +infty by A56, Def12;
hence lim L = (sup (rng J)) + (sup (rng K)) by A9, A39, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose A57: sup (rng J) = +infty ; :: thesis: ( L is convergent & lim L = (sup (rng J)) + (sup (rng K)) )

now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
p <= L . m

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st m <= b₃ holds
n <= L . b₃ )
assume A58: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st m <= b₃ holds
n <= L . b₃

per cases ( sup (rng K) in REAL or sup (rng K) = +infty ) by A4, Lm8;

suppose A59: sup (rng K) in REAL ; :: thesis: ex n being Nat st
for m being Nat st m <= b₃ holds
n <= L . b₃

then reconsider supk = sup (rng K) as Element of REAL ;
reconsider p92 = p / 2, p9 = p as Element of REAL by XREAL_0:def 1;
A60: supk - p92 = (sup (rng K)) - (p / 2) by SUPINF_2:3;
then A61: p9 - (supk - p92) = p - ((sup (rng K)) - (p / 2)) by SUPINF_2:3;
then p - ((sup (rng K)) - (p / 2)) < sup (rng J) by A57, XXREAL_0:9;
then consider j being Element of ExtREAL such that
A62: j in rng J and
A63: p - ((sup (rng K)) - (p / 2)) < j by XXREAL_2:94;
p9 = (p9 - (supk - p92)) + (supk - p92) ;
then A64: (p - ((sup (rng K)) - (p / 2))) + ((sup (rng K)) - (p / 2)) = p9 by A60, A61, SUPINF_2:1;
consider k being ExtReal such that
A65: k in rng K and
A66: (sup (rng K)) - (p / 2) < k by A58, A59, MEASURE6:6;
consider n1 being object such that
A67: n1 in dom K and
A68: k = K . n1 by A65, FUNCT_1:def 3;
consider n2 being object such that
A69: n2 in dom J and
A70: j = J . n2 by A62, FUNCT_1:def 3;
reconsider n1 = n1 as Element of NAT by A67;
reconsider n2 = n2 as Element of NAT by A69;
set n = max (n1,n2);
J . n2 <= J . (max (n1,n2)) by A1, XXREAL_0:25;
then A71: p - ((sup (rng K)) - (p / 2)) < J . (max (n1,n2)) by A63, A70, XXREAL_0:2;
K . n1 <= K . (max (n1,n2)) by A2, XXREAL_0:25;
then A72: (sup (rng K)) - (p / 2) < K . (max (n1,n2)) by A66, A68, XXREAL_0:2;
A73: p < (J . (max (n1,n2))) + (K . (max (n1,n2))) by A72, A71, A64, XXREAL_3:64;

now :: thesis: for m being Nat st max (n1,n2) <= m holds
p <= L . m

let m be Nat; :: thesis: ( max (n1,n2) <= m implies p <= L . m )
assume A74: max (n1,n2) <= m ; :: thesis: p <= L . m
then A75: K . (max (n1,n2)) <= K . m by A2;
J . (max (n1,n2)) <= J . m by A1, A74;
then (J . (max (n1,n2))) + (K . (max (n1,n2))) <= (J . m) + (K . m) by A75, XXREAL_3:36;
then (J . (max (n1,n2))) + (K . (max (n1,n2))) <= L . m by A5;
hence p <= L . m by A73, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
p <= L . m ; :: thesis: verum

end;

suppose sup (rng K) = +infty ; :: thesis: ex n being Nat st
for m being Nat st m <= b₃ holds
n <= L . b₃

then consider n1 being Nat such that
A76: p / 2 < K . n1 by A4, A58, Th59;
consider n2 being Nat such that
A77: p / 2 < J . n2 by A3, A57, A58, Th59;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;
set n = max (n1,n2);
K . n1 <= K . (max (n1,n2)) by A2, XXREAL_0:25;
then A78: p / 2 < K . (max (n1,n2)) by A76, XXREAL_0:2;
J . n2 <= J . (max (n1,n2)) by A1, XXREAL_0:25;
then A79: p / 2 < J . (max (n1,n2)) by A77, XXREAL_0:2;
(p / 2) + (p / 2) < (J . (max (n1,n2))) + (K . (max (n1,n2))) by A79, A78, XXREAL_3:64;
then p < (J . (max (n1,n2))) + (K . (max (n1,n2))) ;
then A80: p < L . (max (n1,n2)) by A5;

now :: thesis: for m being Nat st max (n1,n2) <= m holds
p <= L . m

let m be Nat; :: thesis: ( max (n1,n2) <= m implies p <= L . m )
assume A81: max (n1,n2) <= m ; :: thesis: p <= L . m
then A82: K . (max (n1,n2)) <= K . m by A2;
J . (max (n1,n2)) <= J . m by A1, A81;
then (J . (max (n1,n2))) + (K . (max (n1,n2))) <= (J . m) + (K . m) by A82, XXREAL_3:36;
then (J . (max (n1,n2))) + (K . (max (n1,n2))) <= L . m by A5;
then L . (max (n1,n2)) <= L . m by A5;
hence p <= L . m by A80, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
p <= L . m ; :: thesis: verum

end;

end;

end;

then A83: L is convergent_to_+infty ;
hence L is convergent ; :: thesis: lim L = (sup (rng J)) + (sup (rng K))
then A84: lim L = +infty by A83, Def12;
A85: K . 0 <= sup (rng K) by A6, FUNCT_1:3, XXREAL_2:4;
-infty < K . 0 by A4;
hence lim L = (sup (rng J)) + (sup (rng K)) by A57, A84, A85, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

hence L is convergent ; :: thesis: ( lim L = sup (rng L) & lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )

A86: now :: thesis: for n, m being Nat st n <= m holds
L . n <= L . m

let n, m be Nat; :: thesis: ( n <= m implies L . n <= L . m )
assume A87: n <= m ; :: thesis: L . n <= L . m
then A88: K . n <= K . m by A2;
J . n <= J . m by A1, A87;
then (J . n) + (K . n) <= (J . m) + (K . m) by A88, XXREAL_3:36;
then L . n <= (J . m) + (K . m) by A5;
hence L . n <= L . m by A5; :: thesis: verum

end;

hence lim L = sup (rng L) by Th54; :: thesis: ( lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )
lim J = sup (rng J) by A1, Th54;
hence ( lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) ) by A2, A8, A86, Th54; :: thesis: verum