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 without-infty & K is without-infty & ( 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 without-infty and
A4: K is without-infty 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

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 number ;

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 number ;

A11: now

let p be real number ; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (R_EAL (SJ + SK))).| < p )
assume A12: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (R_EAL (SJ + SK))).| < p
then consider SJ9 being ext-real number such that
A13: SJ9 in rng J and
A14: (sup (rng J)) - (R_EAL (p / 2)) < SJ9 by A9, MEASURE6:6;
consider nj being set 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 ext-real number such that
A17: SK9 in rng K and
A18: (sup (rng K)) - (R_EAL (p / 2)) < SK9 by A10, A12, MEASURE6:6;
consider nk being set 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) - (R_EAL (SJ + SK))).| < p
(p / 2) + (p / 2) = p ;
then A21: R_EAL p = (R_EAL (p / 2)) + (R_EAL (p / 2)) by SUPINF_2:1;

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

end;

end;

then A38: L is convergent_to_finite_number by Def8;
hence L is convergent by Def11; :: 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 number 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 Real by A9;
let p be real number ; :: 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 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 ext-real number such that
A40: j in rng J and
A41: (sup (rng J)) - (R_EAL (p / 2)) < j by A9, MEASURE6:6;
consider n1 being set such that
A42: n1 in dom J and
A43: j = J . n1 by A40, FUNCT_1:def 3;
A44: supj - p92 = (sup (rng J)) - (R_EAL (p / 2)) by SUPINF_2:3;
then A45: p9 - (supj - p92) = (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) by SUPINF_2:3;
then (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) < sup (rng K) by A39, XXREAL_0:9;
then consider k being R_eal such that
A46: k in rng K and
A47: (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) < k by XXREAL_2:94;
p9 = (p9 - (supj - p92)) + (supj - p92) ;
then A48: ((R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2)))) + ((sup (rng J)) - (R_EAL (p / 2))) = p9 by A44, A45, SUPINF_2:1;
reconsider n1 = n1 as Element of NAT by A42;
consider n2 being set 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)) - (R_EAL (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: (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) < K . (max (n1,n2)) by A47, A50, XXREAL_0:2;
-infty < (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) by A45, XXREAL_0:12;
then A53: R_EAL p < (J . (max (n1,n2))) + (K . (max (n1,n2))) by A51, A52, A48, XXREAL_3:64;

now

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 by Def9;
hence L is convergent by Def11; :: 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

let p be real number ; :: 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 Real ;
reconsider p92 = p / 2, p9 = p as Real by XREAL_0:def 1;
A60: supk - p92 = (sup (rng K)) - (R_EAL (p / 2)) by SUPINF_2:3;
then A61: p9 - (supk - p92) = (R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2))) by SUPINF_2:3;
then (R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2))) < sup (rng J) by A57, XXREAL_0:9;
then consider j being R_eal such that
A62: j in rng J and
A63: (R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2))) < j by XXREAL_2:94;
p9 = (p9 - (supk - p92)) + (supk - p92) ;
then A64: ((R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2)))) + ((sup (rng K)) - (R_EAL (p / 2))) = p9 by A60, A61, SUPINF_2:1;
consider k being ext-real number such that
A65: k in rng K and
A66: (sup (rng K)) - (R_EAL (p / 2)) < k by A58, A59, MEASURE6:6;
consider n1 being set such that
A67: n1 in dom K and
A68: k = K . n1 by A65, FUNCT_1:def 3;
consider n2 being set 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: (R_EAL p) - ((sup (rng K)) - (R_EAL (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)) - (R_EAL (p / 2)) < K . (max (n1,n2)) by A66, A68, XXREAL_0:2;
-infty < (R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2))) by A61, XXREAL_0:12;
then A73: R_EAL p < (J . (max (n1,n2))) + (K . (max (n1,n2))) by A72, A71, A64, XXREAL_3:64;

now

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: R_EAL (p / 2) < K . n1 by A4, A58, Th65;
consider n2 being Nat such that
A77: R_EAL (p / 2) < J . n2 by A3, A57, A58, Th65;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;
set n = max (n1,n2);
A78: (p / 2) + (p / 2) = p ;
K . n1 <= K . (max (n1,n2)) by A2, XXREAL_0:25;
then A79: R_EAL (p / 2) < K . (max (n1,n2)) by A76, XXREAL_0:2;
J . n2 <= J . (max (n1,n2)) by A1, XXREAL_0:25;
then A80: R_EAL (p / 2) < J . (max (n1,n2)) by A77, XXREAL_0:2;
-infty < R_EAL (p / 2) by XXREAL_0:12;
then (R_EAL (p / 2)) + (R_EAL (p / 2)) < (J . (max (n1,n2))) + (K . (max (n1,n2))) by A80, A79, XXREAL_3:64;
then p < (J . (max (n1,n2))) + (K . (max (n1,n2))) by A78, SUPINF_2:1;
then A81: R_EAL p < L . (max (n1,n2)) by A5;

now

let m be Nat; :: thesis: ( max (n1,n2) <= m implies p <= L . m )
assume A82: max (n1,n2) <= m ; :: thesis: p <= L . m
then A83: K . (max (n1,n2)) <= K . m by A2;
J . (max (n1,n2)) <= J . m by A1, A82;
then (J . (max (n1,n2))) + (K . (max (n1,n2))) <= (J . m) + (K . m) by A83, 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 A81, 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 A84: L is convergent_to_+infty by Def9;
hence L is convergent by Def11; :: thesis: lim L = (sup (rng J)) + (sup (rng K))
then A85: lim L = +infty by A84, Def12;
A86: K . 0 <= sup (rng K) by A6, FUNCT_1:3, XXREAL_2:4;
-infty < K . 0 by A4, Def5;
hence lim L = (sup (rng J)) + (sup (rng K)) by A57, A85, A86, 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)) )

A87: now

let n, m be Nat; :: thesis: ( n <= m implies L . n <= L . m )
assume A88: n <= m ; :: thesis: L . n <= L . m
then A89: K . n <= K . m by A2;
J . n <= J . m by A1, A88;
then (J . n) + (K . n) <= (J . m) + (K . m) by A89, 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 Th60; :: thesis: ( lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )
lim J = sup (rng J) by A1, Th60;
hence ( lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) ) by A2, A8, A87, Th60; :: thesis: verum