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;

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

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)) )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)) )per cases
( sup (rng J) in REAL or sup (rng J) = +infty )
by A3, Lm8;

end;

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 ;

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

end;

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 ;

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

then A38:
L is convergent_to_finite_number
;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

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

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

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

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;ex n being Nat st

for m being Nat st n <= m holds

p <= L . m

proof

then A56:
L is convergent_to_+infty
;
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;

for m being Nat st n <= m holds

p <= L . m ; :: thesis: verum

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

hence
ex n being Nat st 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;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

for m being Nat st n <= m holds

p <= L . m ; :: thesis: verum

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

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

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;

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

then A83:
L is convergent_to_+infty
;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_{3} holds

n <= L . b_{3} )

assume A58: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st m <= b_{3} holds

n <= L . b_{3}

end;for m being Nat st m <= b

n <= L . b

assume A58: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st m <= b

n <= L . b

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

end;

suppose A59:
sup (rng K) in REAL
; :: thesis: ex n being Nat st

for m being Nat st m <= b_{3} holds

n <= L . b_{3}

for m being Nat st m <= b

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;

for m being Nat st n <= m holds

p <= L . m ; :: thesis: verum

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

hence
ex n being Nat st 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;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

for m being Nat st n <= m holds

p <= L . m ; :: thesis: verum

suppose
sup (rng K) = +infty
; :: thesis: ex n being Nat st

for m being Nat st m <= b_{3} holds

n <= L . b_{3}

for m being Nat st m <= b

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;

for m being Nat st n <= m holds

p <= L . m ; :: thesis: verum

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

hence
ex n being Nat st 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;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

for m being Nat st n <= m holds

p <= L . m ; :: thesis: verum

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

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

L . n <= L . m

hence
lim L = sup (rng L)
by Th54; :: thesis: ( lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )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;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

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