let f be Function of [:NAT,NAT:],ExtREAL; for f1, f2 being without-infty Function of [:NAT,NAT:],ExtREAL st ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & ( for n, m being Nat holds (f1 . (n,m)) + (f2 . (n,m)) = f . (n,m) ) holds
( f is P-convergent & P-lim f = sup (rng f) & P-lim f = (P-lim f1) + (P-lim f2) & sup (rng f) = (sup (rng f1)) + (sup (rng f2)) )
let f1, f2 be without-infty Function of [:NAT,NAT:],ExtREAL; ( ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & ( for n, m being Nat holds (f1 . (n,m)) + (f2 . (n,m)) = f . (n,m) ) implies ( f is P-convergent & P-lim f = sup (rng f) & P-lim f = (P-lim f1) + (P-lim f2) & sup (rng f) = (sup (rng f1)) + (sup (rng f2)) ) )
assume that
A1:
for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2)
and
A2:
for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2)
and
A5:
for n, m being Nat holds (f1 . (n,m)) + (f2 . (n,m)) = f . (n,m)
; ( f is P-convergent & P-lim f = sup (rng f) & P-lim f = (P-lim f1) + (P-lim f2) & sup (rng f) = (sup (rng f1)) + (sup (rng f2)) )
A6:
( dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] )
by FUNCT_2:def 1;
B0:
( f1 is P-convergent & P-lim f1 = sup (rng f1) & f2 is P-convergent & P-lim f2 = sup (rng f2) )
by A1, A2, Th96;
now for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f . (n1,m1) <= f . (n2,m2)let n1,
m1,
n2,
m2 be
Nat;
( n1 <= n2 & m1 <= m2 implies f . (n1,m1) <= f . (n2,m2) )assume
(
n1 <= n2 &
m1 <= m2 )
;
f . (n1,m1) <= f . (n2,m2)then
(
f1 . (
n1,
m1)
<= f1 . (
n2,
m2) &
f2 . (
n1,
m1)
<= f2 . (
n2,
m2) )
by A1, A2;
then
(f1 . (n1,m1)) + (f2 . (n1,m1)) <= (f1 . (n2,m2)) + (f2 . (n2,m2))
by XXREAL_3:36;
then
f . (
n1,
m1)
<= (f1 . (n2,m2)) + (f2 . (n2,m2))
by A5;
hence
f . (
n1,
m1)
<= f . (
n2,
m2)
by A5;
verum end;
hence A7:
( f is P-convergent & P-lim f = sup (rng f) )
by Th96; ( P-lim f = (P-lim f1) + (P-lim f2) & sup (rng f) = (sup (rng f1)) + (sup (rng f2)) )
P1:
now P-lim f = (P-lim f1) + (P-lim f2)per cases
( sup (rng f1) in REAL or sup (rng f1) = +infty )
by Lm8;
suppose A9:
sup (rng f1) in REAL
;
P-lim f = (P-lim f1) + (P-lim f2)set SE1 =
sup (rng f1);
per cases
( sup (rng f2) in REAL or sup (rng f2) = +infty )
by Lm8;
suppose A10:
sup (rng f2) in REAL
;
P-lim f = (P-lim f1) + (P-lim f2)set SE2 =
sup (rng f2);
B1:
now for p being Real st 0 < p holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - ((sup (rng f1)) + (sup (rng f2)))).| < plet p be
Real;
( 0 < p implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - ((sup (rng f1)) + (sup (rng f2)))).| < p )assume A11:
0 < p
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - ((sup (rng f1)) + (sup (rng f2)))).| < pthen consider x1 being
ExtReal such that A12:
(
x1 in rng f1 &
(sup (rng f1)) - (p / 2) < x1 )
by A9, MEASURE6:6;
consider z1 being
object such that A13:
(
z1 in dom f1 &
x1 = f1 . z1 )
by A12, FUNCT_1:def 3;
consider n1,
m1 being
object such that A14:
(
n1 in NAT &
m1 in NAT &
z1 = [n1,m1] )
by A13, ZFMISC_1:def 2;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by A14;
consider x2 being
ExtReal such that A15:
(
x2 in rng f2 &
(sup (rng f2)) - (p / 2) < x2 )
by A10, A11, MEASURE6:6;
consider z2 being
object such that A16:
(
z2 in dom f2 &
x2 = f2 . z2 )
by A15, FUNCT_1:def 3;
consider n2,
m2 being
object such that A17:
(
n2 in NAT &
m2 in NAT &
z2 = [n2,m2] )
by A16, ZFMISC_1:def 2;
reconsider n2 =
n2,
m2 =
m2 as
Element of
NAT by A17;
reconsider N =
max (
(max (n1,m1)),
(max (n2,m2))) as
Nat ;
take N =
N;
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - ((sup (rng f1)) + (sup (rng f2)))).| < phereby verum
let n,
m be
Nat;
( n >= N & m >= N implies |.((f . (n,m)) - ((sup (rng f1)) + (sup (rng f2)))).| < p )assume A18:
(
n >= N &
m >= N )
;
|.((f . (n,m)) - ((sup (rng f1)) + (sup (rng f2)))).| < p
(
N >= max (
n1,
m1) &
N >= max (
n2,
m2) &
max (
n1,
m1)
>= n1 &
max (
n1,
m1)
>= m1 &
max (
n2,
m2)
>= n2 &
max (
n2,
m2)
>= m2 )
by XXREAL_0:25;
then
(
N >= n1 &
N >= m1 &
N >= n2 &
N >= m2 )
by XXREAL_0:2;
then
(
n >= n1 &
n >= n2 &
m >= m1 &
m >= m2 )
by A18, XXREAL_0:2;
then A22:
(
f1 . (
n1,
m1)
<= f1 . (
n,
m) &
f2 . (
n2,
m2)
<= f2 . (
n,
m) )
by A1, A2;
then
(
(sup (rng f1)) - (f1 . (n,m)) <= (sup (rng f1)) - x1 &
(sup (rng f2)) - (f2 . (n,m)) <= (sup (rng f2)) - x2 )
by A13, A14, A16, A17, XXREAL_3:37;
then A19:
((sup (rng f1)) - (f1 . (n,m))) + ((sup (rng f2)) - (f2 . (n,m))) <= ((sup (rng f1)) - x1) + ((sup (rng f2)) - x2)
by XXREAL_3:36;
A20:
p / 2
in REAL
by XREAL_0:def 1;
(
sup (rng f1) < (p / 2) + x1 &
sup (rng f2) < (p / 2) + x2 )
by A12, A15, XXREAL_3:54;
then A21:
(
(sup (rng f1)) - x1 < p / 2 &
(sup (rng f2)) - x2 < p / 2 )
by XXREAL_3:55;
then A24:
(p / 2) + ((sup (rng f2)) - x2) < (p / 2) + (p / 2)
by A20, XXREAL_3:43;
(
n in NAT &
m in NAT )
by ORDINAL1:def 12;
then
[n,m] in [:NAT,NAT:]
by ZFMISC_1:87;
then B1:
(
f1 . (
n,
m)
in rng f1 &
f2 . (
n,
m)
in rng f2 &
f1 . (
n,
m)
<= sup (rng f1) &
f2 . (
n,
m)
<= sup (rng f2) )
by A6, FUNCT_1:3, XXREAL_2:4;
then B2:
(
f1 . (
n,
m)
< +infty &
f2 . (
n,
m)
< +infty )
by A9, A10, XXREAL_0:2, XXREAL_0:9;
B3:
(
-infty <> f1 . (
n,
m) &
-infty <> f2 . (
n,
m) )
by B1, MESFUNC5:def 3;
(
-infty <> x1 &
-infty <> x2 )
by A12, A15, MESFUNC5:def 3;
then
(
x1 in REAL &
x2 in REAL )
by B2, A22, A13, A14, A16, A17, XXREAL_0:14;
then
(sup (rng f2)) - x2 in REAL
by A10, XREAL_0:def 1;
then
((sup (rng f1)) - x1) + ((sup (rng f2)) - x2) < (p / 2) + ((sup (rng f2)) - x2)
by A21, XXREAL_3:43;
then
((sup (rng f1)) - x1) + ((sup (rng f2)) - x2) < (p / 2) + (p / 2)
by A24, XXREAL_0:2;
then A26:
((sup (rng f1)) - (f1 . (n,m))) + ((sup (rng f2)) - (f2 . (n,m))) < p
by A19, XXREAL_0:2;
B5:
((sup (rng f1)) - (f1 . (n,m))) + ((sup (rng f2)) - (f2 . (n,m))) =
(((sup (rng f1)) - (f1 . (n,m))) + (sup (rng f2))) - (f2 . (n,m))
by A10, B2, B3, XXREAL_3:30
.=
(((sup (rng f2)) + (sup (rng f1))) - (f1 . (n,m))) - (f2 . (n,m))
by A9, A10, XXREAL_3:30
.=
((sup (rng f1)) + (sup (rng f2))) - ((f1 . (n,m)) + (f2 . (n,m)))
by A9, A10, B3, XXREAL_3:31
.=
((sup (rng f1)) + (sup (rng f2))) - (f . (n,m))
by A5
;
(
(sup (rng f1)) - (f1 . (n,m)) >= 0 &
(sup (rng f2)) - (f2 . (n,m)) >= 0 )
by B1, XXREAL_3:40;
then
|.(((sup (rng f1)) + (sup (rng f2))) - (f . (n,m))).| < p
by B5, A26, EXTREAL1:def 1;
then
|.(- ((f . (n,m)) - ((sup (rng f1)) + (sup (rng f2))))).| < p
by XXREAL_3:26;
hence
|.((f . (n,m)) - ((sup (rng f1)) + (sup (rng f2)))).| < p
by EXTREAL1:29;
verum
end; end; then
f is
P-convergent_to_finite_number
by A9, A10;
hence
P-lim f = (P-lim f1) + (P-lim f2)
by A9, A10, B0, B1, A7, Def5;
verum end; suppose C1:
sup (rng f2) = +infty
;
P-lim f = (P-lim f1) + (P-lim f2)then C2:
(P-lim f1) + (P-lim f2) = +infty
by B0, A9, XXREAL_3:def 2;
now for g being Real st 0 < g holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= f . (n,m)let g be
Real;
( 0 < g implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= f . (n,m) )assume
0 < g
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= f . (n,m)then consider e1 being
ExtReal such that C5:
(
e1 in rng f1 &
(sup (rng f1)) - (g / 2) < e1 )
by A9, MEASURE6:6;
consider z1 being
object such that C6:
(
z1 in dom f1 &
e1 = f1 . z1 )
by C5, FUNCT_1:def 3;
consider n1,
m1 being
object such that C7:
(
n1 in NAT &
m1 in NAT &
z1 = [n1,m1] )
by C6, ZFMISC_1:def 2;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by C7;
(
g - ((sup (rng f1)) - (g / 2)) in REAL &
(sup (rng f1)) - (g / 2) in REAL )
by A9, XREAL_0:def 1;
then consider e2 being
Element of
ExtREAL such that C8:
(
e2 in rng f2 &
g - ((sup (rng f1)) - (g / 2)) < e2 )
by C1, XXREAL_0:9, XXREAL_2:94;
consider z2 being
object such that C9:
(
z2 in dom f2 &
e2 = f2 . z2 )
by C8, FUNCT_1:def 3;
consider n2,
m2 being
object such that C10:
(
n2 in NAT &
m2 in NAT &
z2 = [n2,m2] )
by C9, ZFMISC_1:def 2;
reconsider n2 =
n2,
m2 =
m2 as
Element of
NAT by C10;
reconsider N =
max (
(max (n2,m2)),
(max (n1,m1))) as
Nat ;
take N =
N;
for n, m being Nat st n >= N & m >= N holds
g <= f . (n,m)
(
N >= max (
n1,
m1) &
N >= max (
n2,
m2) &
max (
n1,
m1)
>= n1 &
max (
n1,
m1)
>= m1 &
max (
n2,
m2)
>= n2 &
max (
n2,
m2)
>= m2 )
by XXREAL_0:25;
then C13:
(
N >= n1 &
N >= m1 &
N >= n2 &
N >= m2 )
by XXREAL_0:2;
hereby verum
let n,
m be
Nat;
( n >= N & m >= N implies g <= f . (n,m) )assume
(
n >= N &
m >= N )
;
g <= f . (n,m)then
(
n >= n1 &
m >= m1 &
n >= n2 &
m >= m2 )
by C13, XXREAL_0:2;
then
(
f1 . (
n,
m)
>= f1 . (
n1,
m1) &
f2 . (
n,
m)
>= f2 . (
n2,
m2) )
by A1, A2;
then C14:
(
(sup (rng f1)) - (g / 2) < f1 . (
n,
m) &
g - ((sup (rng f1)) - (g / 2)) < f2 . (
n,
m) )
by C5, C6, C7, C8, C9, C10, XXREAL_0:2;
(g - ((sup (rng f1)) - (g / 2))) + ((sup (rng f1)) - (g / 2)) = g
by A9, XXREAL_3:22;
then
g < (f1 . (n,m)) + (f2 . (n,m))
by C14, XXREAL_3:64;
hence
g <= f . (
n,
m)
by A5;
verum
end; end; then
f is
P-convergent_to_+infty
;
hence
P-lim f = (P-lim f1) + (P-lim f2)
by C2, A7, Def5;
verum end; end; suppose D1:
sup (rng f1) = +infty
;
P-lim f = (P-lim f1) + (P-lim f2)per cases
( sup (rng f2) in REAL or sup (rng f2) = +infty )
by Lm8;
suppose D3:
sup (rng f2) in REAL
;
P-lim f = (P-lim f1) + (P-lim f2)set SE2 =
sup (rng f2);
D2:
(P-lim f1) + (P-lim f2) = +infty
by B0, D1, D3, XXREAL_3:def 2;
now for g being Real st 0 < g holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= f . (n,m)let g be
Real;
( 0 < g implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= f . (n,m) )assume
0 < g
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= f . (n,m)then consider e2 being
ExtReal such that D5:
(
e2 in rng f2 &
(sup (rng f2)) - (g / 2) < e2 )
by D3, MEASURE6:6;
consider z2 being
object such that D6:
(
z2 in dom f2 &
e2 = f2 . z2 )
by D5, FUNCT_1:def 3;
consider n1,
m1 being
object such that D7:
(
n1 in NAT &
m1 in NAT &
z2 = [n1,m1] )
by D6, ZFMISC_1:def 2;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by D7;
(
g - ((sup (rng f2)) - (g / 2)) in REAL &
(sup (rng f2)) - (g / 2) in REAL )
by D3, XREAL_0:def 1;
then consider e1 being
Element of
ExtREAL such that D8:
(
e1 in rng f1 &
g - ((sup (rng f2)) - (g / 2)) < e1 )
by D1, XXREAL_0:9, XXREAL_2:94;
consider z1 being
object such that D9:
(
z1 in dom f1 &
e1 = f1 . z1 )
by D8, FUNCT_1:def 3;
consider n2,
m2 being
object such that D10:
(
n2 in NAT &
m2 in NAT &
z1 = [n2,m2] )
by D9, ZFMISC_1:def 2;
reconsider n2 =
n2,
m2 =
m2 as
Element of
NAT by D10;
reconsider N =
max (
(max (n2,m2)),
(max (n1,m1))) as
Nat ;
take N =
N;
for n, m being Nat st n >= N & m >= N holds
g <= f . (n,m)
(
N >= max (
n1,
m1) &
N >= max (
n2,
m2) &
max (
n1,
m1)
>= n1 &
max (
n1,
m1)
>= m1 &
max (
n2,
m2)
>= n2 &
max (
n2,
m2)
>= m2 )
by XXREAL_0:25;
then D13:
(
N >= n1 &
N >= m1 &
N >= n2 &
N >= m2 )
by XXREAL_0:2;
hereby verum
let n,
m be
Nat;
( n >= N & m >= N implies g <= f . (n,m) )assume
(
n >= N &
m >= N )
;
g <= f . (n,m)then
(
n >= n1 &
m >= m1 &
n >= n2 &
m >= m2 )
by D13, XXREAL_0:2;
then
(
f1 . (
n,
m)
>= f1 . (
n2,
m2) &
f2 . (
n,
m)
>= f2 . (
n1,
m1) )
by A1, A2;
then D14:
(
(sup (rng f2)) - (g / 2) < f2 . (
n,
m) &
g - ((sup (rng f2)) - (g / 2)) < f1 . (
n,
m) )
by D5, D6, D7, D8, D9, D10, XXREAL_0:2;
(g - ((sup (rng f2)) - (g / 2))) + ((sup (rng f2)) - (g / 2)) = g
by D3, XXREAL_3:22;
then
g < (f1 . (n,m)) + (f2 . (n,m))
by D14, XXREAL_3:64;
hence
g <= f . (
n,
m)
by A5;
verum
end; end; then
f is
P-convergent_to_+infty
;
hence
P-lim f = (P-lim f1) + (P-lim f2)
by D2, A7, Def5;
verum end; suppose E1:
sup (rng f2) = +infty
;
P-lim f = (P-lim f1) + (P-lim f2)now for p being Real st 0 < p holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
p <= f . (n,m)let p be
Real;
( 0 < p implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
p <= f . (n,m) )assume E2:
0 < p
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
p <= f . (n,m)then consider n1,
m1 being
Nat such that E3:
f1 . (
n1,
m1)
> p / 2
by D1, Th101;
consider n2,
m2 being
Nat such that E4:
f2 . (
n2,
m2)
> p / 2
by E1, E2, Th101;
reconsider n1 =
n1,
n2 =
n2,
m1 =
m1,
m2 =
m2 as
Element of
NAT by ORDINAL1:def 12;
reconsider N =
max (
(max (n2,m2)),
(max (n1,m1))) as
Nat ;
take N =
N;
for n, m being Nat st n >= N & m >= N holds
p <= f . (n,m)
(
N >= max (
n1,
m1) &
N >= max (
n2,
m2) &
max (
n1,
m1)
>= n1 &
max (
n1,
m1)
>= m1 &
max (
n2,
m2)
>= n2 &
max (
n2,
m2)
>= m2 )
by XXREAL_0:25;
then E5:
(
N >= n1 &
N >= m1 &
N >= n2 &
N >= m2 )
by XXREAL_0:2;
hereby verum
let n,
m be
Nat;
( n >= N & m >= N implies p <= f . (n,m) )assume
(
n >= N &
m >= N )
;
p <= f . (n,m)then
(
n >= n1 &
m >= m1 &
n >= n2 &
m >= m2 )
by E5, XXREAL_0:2;
then
(
f1 . (
n,
m)
>= f1 . (
n1,
m1) &
f2 . (
n,
m)
>= f2 . (
n2,
m2) )
by A1, A2;
then
(
f1 . (
n,
m)
>= p / 2 &
f2 . (
n,
m)
>= p / 2 )
by E3, E4, XXREAL_0:2;
then
(p / 2) + (p / 2) <= (f1 . (n,m)) + (f2 . (n,m))
by XXREAL_3:36;
hence
p <= f . (
n,
m)
by A5;
verum
end; end; then
f is
P-convergent_to_+infty
;
then
(
P-lim f = +infty &
P-lim f1 = +infty &
P-lim f2 = +infty )
by A7, Def5, D1, E1, A1, A2, Th96;
hence
P-lim f = (P-lim f1) + (P-lim f2)
by XXREAL_3:def 2;
verum
hence
P-lim f = (P-lim f1) + (P-lim f2)
; sup (rng f) = (sup (rng f1)) + (sup (rng f2))
P2:
( P-lim f1 = sup (rng f1) & P-lim f2 = sup (rng f2) )
by A1, A2, Th96;
now for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f . (n1,m1) <= f . (n2,m2)let n1,
m1,
n2,
m2 be
Nat;
( n1 <= n2 & m1 <= m2 implies f . (n1,m1) <= f . (n2,m2) )assume
(
n1 <= n2 &
m1 <= m2 )
;
f . (n1,m1) <= f . (n2,m2)then
(
f1 . (
n1,
m1)
<= f1 . (
n2,
m2) &
f2 . (
n1,
m1)
<= f2 . (
n2,
m2) )
by A1, A2;
then
(f1 . (n1,m1)) + (f2 . (n1,m1)) <= (f1 . (n2,m2)) + (f2 . (n2,m2))
by XXREAL_3:36;
then
f . (
n1,
m1)
<= (f1 . (n2,m2)) + (f2 . (n2,m2))
by A5;
hence
f . (
n1,
m1)
<= f . (
n2,
m2)
by A5;
verum end;
hence
sup (rng f) = (sup (rng f1)) + (sup (rng f2))
by P1, P2, Th96; verum