= -(seq.m) by A8,XXREAL_3:38; then
A9: --g >= -(seq.m) by XXREAL_3:def 3;
m in NAT by ORDINAL1:def 12; then
m in dom(-seq) by FUNCT_2:def 1;
hence (-seq).m <= g by A9,MESFUNC1:def 7;
end;
end;
hence -seq is convergent_to_-infty by MESFUNC5:def 10;
hence -seq is convergent;
lim(-seq) = -infty & lim seq = +infty by A6,A10,MESFUNC9:7,MESFUNC5:def 10;
hence lim (-seq) = - lim seq by XXREAL_3:6;
end;
thus seq is convergent_to_+infty
implies -seq is convergent_to_-infty by P1;
P2:now assume A11: seq is convergent_to_-infty;
A15:now let g be Real;
assume A12: g > 0;
reconsider p = -g as ExtReal;
consider n be Nat such that
A13: for m be Nat st n <= m holds seq.m <= p by A11,A12,MESFUNC5:def 10;
take n;
hereby let m be Nat;
assume n<=m; then
-(seq.m) >= -p by A13,XXREAL_3:38; then
A14: -(seq.m) >= --g by XXREAL_3:def 3;
m in NAT by ORDINAL1:def 12; then
m in dom(-seq) by FUNCT_2:def 1;
hence (-seq).m >= g by A14,MESFUNC1:def 7;
end;
end;
hence -seq is convergent_to_+infty by MESFUNC5:def 9;
hence -seq is convergent;
lim(-seq) = +infty & lim seq = -infty by A11,A15,MESFUNC9:7,MESFUNC5:def 9;
hence lim (-seq) = - lim seq by XXREAL_3:5;
end;
thus seq is convergent_to_-infty
implies -seq is convergent_to_+infty by P2;
thus thesis by P0,P1,P2,MESFUNC5:def 11;
end;
theorem Th17:
for seq be convergent ExtREAL_sequence holds
(seq is convergent_to_finite_number iff -seq is convergent_to_finite_number)
& (seq is convergent_to_+infty iff -seq is convergent_to_-infty)
& (seq is convergent_to_-infty iff -seq is convergent_to_+infty)
& -seq is convergent & lim (-seq) = - lim seq
proof
let seq be convergent ExtREAL_sequence;
now assume -seq is convergent_to_finite_number; then
-(-seq) is convergent_to_finite_number by Lm6;
hence seq is convergent_to_finite_number by Th2;
end;
hence seq is convergent_to_finite_number
iff -seq is convergent_to_finite_number by Lm6;
now assume -seq is convergent_to_-infty; then
-(-seq) is convergent_to_+infty by Lm6;
hence seq is convergent_to_+infty by Th2;
end;
hence seq is convergent_to_+infty iff -seq is convergent_to_-infty by Lm6;
now assume -seq is convergent_to_+infty; then
-(-seq) is convergent_to_-infty by Lm6;
hence seq is convergent_to_-infty by Th2;
end;
hence seq is convergent_to_-infty iff -seq is convergent_to_+infty by Lm6;
thus -seq is convergent & lim (-seq) = - lim seq by Lm6;
end;
theorem Th18:
for seq1,seq2 be without-infty ExtREAL_sequence
st seq1 is convergent_to_+infty & seq2 is convergent_to_+infty
holds seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent
& lim(seq1+seq2) = +infty
proof
let seq1,seq2 be without-infty ExtREAL_sequence;
assume A1: seq1 is convergent_to_+infty & seq2 is convergent_to_+infty;
now let g be Real;
assume A2: 0 < g; then
consider n1 be Nat such that
A3: for m be Nat st n1<=m holds g/2<=seq1.m by A1,MESFUNC5:def 9;
consider n2 be Nat such that
A4: for m be Nat st n2<=m holds g/2<=seq2.m by A1,A2,MESFUNC5:def 9;
reconsider N1=n1, N2=n2 as Element of NAT by ORDINAL1:def 12;
reconsider n = max(N1,N2) as Nat;
A5: n1<=n & n2<=n by XXREAL_0:25;
now let m be Nat;
assume n<=m; then
n1<=m & n2<=m by A5,XXREAL_0:2; then
g/2 <= seq1.m & g/2 <= seq2.m by A3,A4; then
A6: g/2 + g/2 <= seq1.m + seq2.m by XXREAL_3:36;
m is Element of NAT by ORDINAL1:def 12;
hence g<=(seq1+seq2).m by A6,Th7;
end;
hence ex n be Nat st for m be Nat st n<=m holds g <= (seq1+seq2).m;
end;
hence
A7: seq1+seq2 is convergent_to_+infty by MESFUNC5:def 9;
hence seq1+seq2 is convergent;
thus lim(seq1+seq2) = +infty by A7,MESFUNC5:def 12;
end;
theorem Th19:
for seq1,seq2 be without-infty ExtREAL_sequence
st seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number
holds seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent
& lim(seq1+seq2)=+infty
proof
let seq1,seq2 be without-infty ExtREAL_sequence;
assume
A1: seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number; then
consider S2 be Real such that
A2: for g be Real st 0

=N & m>=N holds |. Eseq.(n,m) - (p qua ExtReal) .| < e; attr Eseq is P-convergent_to_+infty means for g be Real st 0 < g ex N be Nat st for n,m be Nat st n>=N & m>=N holds g <= Eseq.(n,m); attr Eseq is P-convergent_to_-infty means for g be Real st g < 0 ex N be Nat st for n,m be Nat st n>=N & m>=N holds Eseq.(n,m) <= g; end; definition let f be Function of [:NAT,NAT:],ExtREAL; attr f is convergent_in_cod1_to_+infty means for m be Element of NAT holds ProjMap2(f,m) is convergent_to_+infty; attr f is convergent_in_cod1_to_-infty means for m be Element of NAT holds ProjMap2(f,m) is convergent_to_-infty; attr f is convergent_in_cod1_to_finite means for m be Element of NAT holds ProjMap2(f,m) is convergent_to_finite_number; attr f is convergent_in_cod1 means for m be Element of NAT holds ProjMap2(f,m) is convergent; attr f is convergent_in_cod2_to_+infty means for m be Element of NAT holds ProjMap1(f,m) is convergent_to_+infty; attr f is convergent_in_cod2_to_-infty means for m be Element of NAT holds ProjMap1(f,m) is convergent_to_-infty; attr f is convergent_in_cod2_to_finite means for m be Element of NAT holds ProjMap1(f,m) is convergent_to_finite_number; attr f is convergent_in_cod2 means for m be Element of NAT holds ProjMap1(f,m) is convergent; end; theorem for f be Function of [:NAT,NAT:],ExtREAL holds ( f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty or f is convergent_in_cod1_to_finite implies f is convergent_in_cod1 ) & ( f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or f is convergent_in_cod2_to_finite implies f is convergent_in_cod2 ) proof let f be Function of [:NAT,NAT:],ExtREAL; hereby assume A1: f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty or f is convergent_in_cod1_to_finite; per cases by A1; suppose A2: f is convergent_in_cod1_to_+infty; now let m be Element of NAT; ProjMap2(f,m) is convergent_to_+infty by A2; hence ProjMap2(f,m) is convergent; end; hence f is convergent_in_cod1; end; suppose A3: f is convergent_in_cod1_to_-infty; now let m be Element of NAT; ProjMap2(f,m) is convergent_to_-infty by A3; hence ProjMap2(f,m) is convergent; end; hence f is convergent_in_cod1; end; suppose A4: f is convergent_in_cod1_to_finite; now let m be Element of NAT; ProjMap2(f,m) is convergent_to_finite_number by A4; hence ProjMap2(f,m) is convergent; end; hence f is convergent_in_cod1; end; end; assume A5: f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or f is convergent_in_cod2_to_finite; per cases by A5; suppose A6: f is convergent_in_cod2_to_+infty; now let m be Element of NAT; ProjMap1(f,m) is convergent_to_+infty by A6; hence ProjMap1(f,m) is convergent; end; hence f is convergent_in_cod2; end; suppose A7: f is convergent_in_cod2_to_-infty; now let m be Element of NAT; ProjMap1(f,m) is convergent_to_-infty by A7; hence ProjMap1(f,m) is convergent; end; hence f is convergent_in_cod2; end; suppose A8: f is convergent_in_cod2_to_finite; now let m be Element of NAT; ProjMap1(f,m) is convergent_to_finite_number by A8; hence ProjMap1(f,m) is convergent; end; hence f is convergent_in_cod2; end; end; theorem Th32: for X,Y,Z be non empty set, F be Function of [:X,Y:],Z, x be Element of X holds ProjMap1(F,x) = ProjMap2(F@,x) proof let X,Y,Z be non empty set; let F be Function of [:X,Y:],Z; let x be Element of X; now let y be Element of Y; ProjMap1(F,x).y = F.(x,y) by MESFUNC9:def 6 .= F@.(y,x) by DBLSEQ_2:def 2; hence ProjMap1(F,x).y = ProjMap2(F@,x).y by MESFUNC9:def 7; end; hence ProjMap1(F,x) = ProjMap2(F@,x) by FUNCT_2:def 8; end; theorem Th33: for X,Y,Z be non empty set, F be Function of [:X,Y:],Z, y be Element of Y holds ProjMap2(F,y) = ProjMap1(F@,y) proof let X,Y,Z be non empty set; let F be Function of [:X,Y:],Z; let y be Element of Y; now let x be Element of X; ProjMap2(F,y).x = F.(x,y) by MESFUNC9:def 7 .= F@.(y,x) by DBLSEQ_2:def 2; hence ProjMap2(F,y).x = ProjMap1(F@,y).x by MESFUNC9:def 6; end; hence ProjMap2(F,y) = ProjMap1(F@,y) by FUNCT_2:def 8; end; theorem Th34: for X,Y be non empty set, F be Function of [:X,Y:],ExtREAL, x be Element of X holds ProjMap1(-F,x) = -ProjMap1(F,x) proof let X,Y be non empty set, F be Function of [:X,Y:],ExtREAL, x be Element of X; now let y be Element of Y; [x,y] in [:X,Y:] by ZFMISC_1:87; then A1: [x,y] in dom(-F) by FUNCT_2:def 1; A2: dom(-ProjMap1(F,x)) = Y by FUNCT_2:def 1; ProjMap1(-F,x).y = (-F).(x,y) by MESFUNC9:def 6; then ProjMap1(-F,x).y = -(F.(x,y)) by A1,MESFUNC1:def 7; then ProjMap1(-F,x).y = -(ProjMap1(F,x).y) by MESFUNC9:def 6; hence ProjMap1(-F,x).y = (-ProjMap1(F,x)).y by A2,MESFUNC1:def 7; end; hence ProjMap1(-F,x) = -ProjMap1(F,x) by FUNCT_2:def 8; end; theorem Th35: for X,Y be non empty set, F be Function of [:X,Y:],ExtREAL, y be Element of Y holds ProjMap2(-F,y) = -ProjMap2(F,y) proof let X,Y be non empty set, F be Function of [:X,Y:],ExtREAL, y be Element of Y; now let x be Element of X; [x,y] in [:X,Y:] by ZFMISC_1:87; then A1: [x,y] in dom(-F) by FUNCT_2:def 1; A2: dom(-ProjMap2(F,y)) = X by FUNCT_2:def 1; ProjMap2(-F,y).x = (-F).(x,y) by MESFUNC9:def 7; then ProjMap2(-F,y).x = -(F.(x,y)) by A1,MESFUNC1:def 7; then ProjMap2(-F,y).x = -(ProjMap2(F,y).x) by MESFUNC9:def 7; hence ProjMap2(-F,y).x = (-ProjMap2(F,y)).x by A2,MESFUNC1:def 7; end; hence ProjMap2(-F,y) = -ProjMap2(F,y) by FUNCT_2:def 8; end; theorem Th36: for f be Function of [:NAT,NAT:],ExtREAL holds (f is convergent_in_cod1_to_+infty iff f@ is convergent_in_cod2_to_+infty) & (f is convergent_in_cod2_to_+infty iff f@ is convergent_in_cod1_to_+infty) & (f is convergent_in_cod1_to_-infty iff f@ is convergent_in_cod2_to_-infty) & (f is convergent_in_cod2_to_-infty iff f@ is convergent_in_cod1_to_-infty) & (f is convergent_in_cod1_to_finite iff f@ is convergent_in_cod2_to_finite) & (f is convergent_in_cod2_to_finite iff f@ is convergent_in_cod1_to_finite) proof let f be Function of [:NAT,NAT:],ExtREAL; now hereby assume A1: f is convergent_in_cod1_to_+infty; now let m be Element of NAT; ProjMap2(f,m) = ProjMap1(f@,m) by Th33; hence ProjMap1(f@,m) is convergent_to_+infty by A1; end; hence f@ is convergent_in_cod2_to_+infty; end; assume A2: f@ is convergent_in_cod2_to_+infty; now let m be Element of NAT; ProjMap2(f,m) = ProjMap1(f@,m) by Th33; hence ProjMap2(f,m) is convergent_to_+infty by A2; end; hence f is convergent_in_cod1_to_+infty; end; hence f is convergent_in_cod1_to_+infty iff f@ is convergent_in_cod2_to_+infty; now hereby assume A3: f is convergent_in_cod2_to_+infty; now let m be Element of NAT; ProjMap1(f,m) = ProjMap2(f@,m) by Th32; hence ProjMap2(f@,m) is convergent_to_+infty by A3; end; hence f@ is convergent_in_cod1_to_+infty; end; assume A4: f@ is convergent_in_cod1_to_+infty; now let m be Element of NAT; ProjMap1(f,m) = ProjMap2(f@,m) by Th32; hence ProjMap1(f,m) is convergent_to_+infty by A4; end; hence f is convergent_in_cod2_to_+infty; end; hence f is convergent_in_cod2_to_+infty iff f@ is convergent_in_cod1_to_+infty; now hereby assume A5: f is convergent_in_cod1_to_-infty; now let m be Element of NAT; ProjMap2(f,m) = ProjMap1(f@,m) by Th33; hence ProjMap1(f@,m) is convergent_to_-infty by A5; end; hence f@ is convergent_in_cod2_to_-infty; end; assume A6: f@ is convergent_in_cod2_to_-infty; now let m be Element of NAT; ProjMap2(f,m) = ProjMap1(f@,m) by Th33; hence ProjMap2(f,m) is convergent_to_-infty by A6; end; hence f is convergent_in_cod1_to_-infty; end; hence f is convergent_in_cod1_to_-infty iff f@ is convergent_in_cod2_to_-infty; now hereby assume A7: f is convergent_in_cod2_to_-infty; now let m be Element of NAT; ProjMap1(f,m) = ProjMap2(f@,m) by Th32; hence ProjMap2(f@,m) is convergent_to_-infty by A7; end; hence f@ is convergent_in_cod1_to_-infty; end; assume A8: f@ is convergent_in_cod1_to_-infty; now let m be Element of NAT; ProjMap1(f,m) = ProjMap2(f@,m) by Th32; hence ProjMap1(f,m) is convergent_to_-infty by A8; end; hence f is convergent_in_cod2_to_-infty; end; hence f is convergent_in_cod2_to_-infty iff f@ is convergent_in_cod1_to_-infty; now hereby assume A9: f is convergent_in_cod1_to_finite; now let m be Element of NAT; ProjMap2(f,m) = ProjMap1(f@,m) by Th33; hence ProjMap1(f@,m) is convergent_to_finite_number by A9; end; hence f@ is convergent_in_cod2_to_finite; end; assume A10: f@ is convergent_in_cod2_to_finite; now let m be Element of NAT; ProjMap2(f,m) = ProjMap1(f@,m) by Th33; hence ProjMap2(f,m) is convergent_to_finite_number by A10; end; hence f is convergent_in_cod1_to_finite; end; hence f is convergent_in_cod1_to_finite iff f@ is convergent_in_cod2_to_finite; now hereby assume A11: f is convergent_in_cod2_to_finite; now let m be Element of NAT; ProjMap1(f,m) = ProjMap2(f@,m) by Th32; hence ProjMap2(f@,m) is convergent_to_finite_number by A11; end; hence f@ is convergent_in_cod1_to_finite; end; assume A12: f@ is convergent_in_cod1_to_finite; now let m be Element of NAT; ProjMap1(f,m) = ProjMap2(f@,m) by Th32; hence ProjMap1(f,m) is convergent_to_finite_number by A12; end; hence f is convergent_in_cod2_to_finite; end; hence f is convergent_in_cod2_to_finite iff f@ is convergent_in_cod1_to_finite; end; theorem for f be Function of [:NAT,NAT:],ExtREAL holds (f is convergent_in_cod1_to_+infty iff -f is convergent_in_cod1_to_-infty) & (f is convergent_in_cod1_to_-infty iff -f is convergent_in_cod1_to_+infty) & (f is convergent_in_cod1_to_finite iff -f is convergent_in_cod1_to_finite) & (f is convergent_in_cod2_to_+infty iff -f is convergent_in_cod2_to_-infty) & (f is convergent_in_cod2_to_-infty iff -f is convergent_in_cod2_to_+infty) & (f is convergent_in_cod2_to_finite iff -f is convergent_in_cod2_to_finite) proof let f be Function of [:NAT,NAT:],ExtREAL; now hereby assume A1: f is convergent_in_cod1_to_+infty; now let m be Element of NAT; A2: ProjMap2(f,m) is convergent_to_+infty by A1; -ProjMap2(f,m) = ProjMap2(-f,m) by Th35; hence ProjMap2(-f,m) is convergent_to_-infty by A2,Th17; end; hence -f is convergent_in_cod1_to_-infty; end; assume A3: -f is convergent_in_cod1_to_-infty; now let m be Element of NAT; -ProjMap2(f,m) = ProjMap2(-f,m) by Th35; then -ProjMap2(f,m) is convergent_to_-infty by A3; then -(-ProjMap2(f,m)) is convergent_to_+infty by Th17; hence ProjMap2(f,m) is convergent_to_+infty by Th2; end; hence f is convergent_in_cod1_to_+infty; end; hence f is convergent_in_cod1_to_+infty iff -f is convergent_in_cod1_to_-infty; now hereby assume A1: f is convergent_in_cod1_to_-infty; now let m be Element of NAT; A2: ProjMap2(f,m) is convergent_to_-infty by A1; -ProjMap2(f,m) = ProjMap2(-f,m) by Th35; hence ProjMap2(-f,m) is convergent_to_+infty by A2,Th17; end; hence -f is convergent_in_cod1_to_+infty; end; assume A3: -f is convergent_in_cod1_to_+infty; now let m be Element of NAT; -ProjMap2(f,m) = ProjMap2(-f,m) by Th35; then -ProjMap2(f,m) is convergent_to_+infty by A3; then -(-ProjMap2(f,m)) is convergent_to_-infty by Th17; hence ProjMap2(f,m) is convergent_to_-infty by Th2; end; hence f is convergent_in_cod1_to_-infty; end; hence f is convergent_in_cod1_to_-infty iff -f is convergent_in_cod1_to_+infty; now hereby assume A1: f is convergent_in_cod1_to_finite; now let m be Element of NAT; A2: ProjMap2(f,m) is convergent_to_finite_number by A1; -ProjMap2(f,m) = ProjMap2(-f,m) by Th35; hence ProjMap2(-f,m) is convergent_to_finite_number by A2,Th17; end; hence -f is convergent_in_cod1_to_finite; end; assume A3: -f is convergent_in_cod1_to_finite; now let m be Element of NAT; -ProjMap2(f,m) = ProjMap2(-f,m) by Th35; then -ProjMap2(f,m) is convergent_to_finite_number by A3; then -(-ProjMap2(f,m)) is convergent_to_finite_number by Th17; hence ProjMap2(f,m) is convergent_to_finite_number by Th2; end; hence f is convergent_in_cod1_to_finite; end; hence f is convergent_in_cod1_to_finite iff -f is convergent_in_cod1_to_finite; now hereby assume A1: f is convergent_in_cod2_to_+infty; now let m be Element of NAT; A2: ProjMap1(f,m) is convergent_to_+infty by A1; -ProjMap1(f,m) = ProjMap1(-f,m) by Th34; hence ProjMap1(-f,m) is convergent_to_-infty by A2,Th17; end; hence -f is convergent_in_cod2_to_-infty; end; assume A3: -f is convergent_in_cod2_to_-infty; now let m be Element of NAT; -ProjMap1(f,m) = ProjMap1(-f,m) by Th34; then -ProjMap1(f,m) is convergent_to_-infty by A3; then -(-ProjMap1(f,m)) is convergent_to_+infty by Th17; hence ProjMap1(f,m) is convergent_to_+infty by Th2; end; hence f is convergent_in_cod2_to_+infty; end; hence f is convergent_in_cod2_to_+infty iff -f is convergent_in_cod2_to_-infty; now hereby assume A1: f is convergent_in_cod2_to_-infty; now let m be Element of NAT; A2: ProjMap1(f,m) is convergent_to_-infty by A1; -ProjMap1(f,m) = ProjMap1(-f,m) by Th34; hence ProjMap1(-f,m) is convergent_to_+infty by A2,Th17; end; hence -f is convergent_in_cod2_to_+infty; end; assume A3: -f is convergent_in_cod2_to_+infty; now let m be Element of NAT; -ProjMap1(f,m) = ProjMap1(-f,m) by Th34; then -ProjMap1(f,m) is convergent_to_+infty by A3; then -(-ProjMap1(f,m)) is convergent_to_-infty by Th17; hence ProjMap1(f,m) is convergent_to_-infty by Th2; end; hence f is convergent_in_cod2_to_-infty; end; hence f is convergent_in_cod2_to_-infty iff -f is convergent_in_cod2_to_+infty; now hereby assume A1: f is convergent_in_cod2_to_finite; now let m be Element of NAT; A2: ProjMap1(f,m) is convergent_to_finite_number by A1; -ProjMap1(f,m) = ProjMap1(-f,m) by Th34; hence ProjMap1(-f,m) is convergent_to_finite_number by A2,Th17; end; hence -f is convergent_in_cod2_to_finite; end; assume A3: -f is convergent_in_cod2_to_finite; now let m be Element of NAT; -ProjMap1(f,m) = ProjMap1(-f,m) by Th34; then -ProjMap1(f,m) is convergent_to_finite_number by A3; then -(-ProjMap1(f,m)) is convergent_to_finite_number by Th17; hence ProjMap1(f,m) is convergent_to_finite_number by Th2; end; hence f is convergent_in_cod2_to_finite; end; hence f is convergent_in_cod2_to_finite iff -f is convergent_in_cod2_to_finite; end; definition let f be Function of [:NAT,NAT:],ExtREAL; func lim_in_cod1 f -> ExtREAL_sequence means :D1DEF5: for m be Element of NAT holds it.m = lim ProjMap2(f,m); existence proof defpred P[Element of NAT,set] means $2 = lim ProjMap2(f,$1); A1:for m be Element of NAT ex n be Element of ExtREAL st P[m,n]; consider IT be Function of NAT,ExtREAL such that A2: for m be Element of NAT holds P[m,IT.m] from FUNCT_2:sch 3(A1); take IT; thus thesis by A2; end; uniqueness proof let f1,f2 be Function of NAT,ExtREAL; assume that A3: for m be Element of NAT holds f1.m = lim ProjMap2(f,m) and A4: for m be Element of NAT holds f2.m = lim ProjMap2(f,m); now let m be Element of NAT; thus f1.m = lim ProjMap2(f,m) by A3 .= f2.m by A4; end; hence f1 = f2 by FUNCT_2:63; end; func lim_in_cod2 f -> ExtREAL_sequence means :D1DEF6: for n be Element of NAT holds it.n = lim ProjMap1(f,n); existence proof defpred P[Element of NAT,set] means $2 = lim ProjMap1(f,$1); A1:for m be Element of NAT holds ex n be Element of ExtREAL st P[m,n]; consider IT be Function of NAT,ExtREAL such that A2: for m be Element of NAT holds P[m,IT.m] from FUNCT_2:sch 3(A1); take IT; thus thesis by A2; end; uniqueness proof let f1,f2 be Function of NAT,ExtREAL; assume that A3: for n be Element of NAT holds f1.n = lim ProjMap1(f,n) and A4: for n be Element of NAT holds f2.n = lim ProjMap1(f,n); now let n be Element of NAT; thus f1.n = lim ProjMap1(f,n) by A3 .= f2.n by A4; end; hence f1 = f2 by FUNCT_2:63; end; end; theorem Th38: for f be Function of [:NAT,NAT:],ExtREAL holds lim_in_cod1 f = lim_in_cod2 (f@) & lim_in_cod2 f = lim_in_cod1 (f@) proof let f be Function of [:NAT,NAT:],ExtREAL; now let n be Element of NAT; (lim_in_cod1 f).n = lim ProjMap2(f,n) by D1DEF5 .= lim ProjMap1(f@,n) by Th33; hence (lim_in_cod1 f).n = (lim_in_cod2 (f@)).n by D1DEF6; end; hence lim_in_cod1 f = lim_in_cod2 (f@) by FUNCT_2:def 8; now let n be Element of NAT; (lim_in_cod2 f).n = lim ProjMap1(f,n) by D1DEF6 .= lim ProjMap2(f@,n) by Th32; hence (lim_in_cod2 f).n = (lim_in_cod1 (f@)).n by D1DEF5; end; hence lim_in_cod2 f = lim_in_cod1 (f@) by FUNCT_2:def 8; end; registration let X,Y be non empty set, F be without+infty Function of [:X,Y:],ExtREAL, x be Element of X; cluster ProjMap1(F,x) -> without+infty; correctness proof now let y be object; per cases; suppose not y in dom (ProjMap1(F,x)); hence (ProjMap1(F,x)).y < +infty by FUNCT_1:def 2; end; suppose y in dom (ProjMap1(F,x)); then reconsider y1=y as Element of Y; (ProjMap1(F,x)).y = F.(x,y1) by MESFUNC9:def 6; hence (ProjMap1(F,x)).y < +infty by MESFUNC5:def 6; end; end; hence thesis by MESFUNC5:def 6; end; end; registration let X,Y be non empty set, F be without+infty Function of [:X,Y:],ExtREAL, y be Element of Y; cluster ProjMap2(F,y) -> without+infty; correctness proof now let x be object; per cases; suppose not x in dom (ProjMap2(F,y)); hence (ProjMap2(F,y)).x < +infty by FUNCT_1:def 2; end; suppose x in dom (ProjMap2(F,y)); then reconsider x1=x as Element of X; (ProjMap2(F,y)).x = F.(x1,y) by MESFUNC9:def 7; hence (ProjMap2(F,y)).x < +infty by MESFUNC5:def 6; end; end; hence thesis by MESFUNC5:def 6; end; end; registration let X,Y be non empty set, F be without-infty Function of [:X,Y:],ExtREAL, x be Element of X; cluster ProjMap1(F,x) -> without-infty; correctness proof now let y be object; per cases; suppose not y in dom (ProjMap1(F,x)); hence -infty < (ProjMap1(F,x)).y by FUNCT_1:def 2; end; suppose y in dom (ProjMap1(F,x)); then reconsider y1=y as Element of Y; (ProjMap1(F,x)).y = F.(x,y1) by MESFUNC9:def 6; hence -infty < (ProjMap1(F,x)).y by MESFUNC5:def 5; end; end; hence thesis by MESFUNC5:def 5; end; end; registration let X,Y be non empty set, F be without-infty Function of [:X,Y:],ExtREAL, y be Element of Y; cluster ProjMap2(F,y) -> without-infty; correctness proof now let x be object; per cases; suppose not x in dom (ProjMap2(F,y)); hence -infty < (ProjMap2(F,y)).x by FUNCT_1:def 2; end; suppose x in dom (ProjMap2(F,y)); then reconsider x1=x as Element of X; (ProjMap2(F,y)).x = F.(x1,y) by MESFUNC9:def 7; hence -infty < (ProjMap2(F,y)).x by MESFUNC5:def 5; end; end; hence thesis by MESFUNC5:def 5; end; end; definition let f be Function of [:NAT,NAT:],ExtREAL; func Partial_Sums_in_cod2 f -> Function of [:NAT,NAT:],ExtREAL means :DefCSM: for n,m be Nat holds it.(n,0) = f.(n,0) & it.(n,m+1) = it.(n,m) + f.(n,m+1); existence proof deffunc F0(Element of NAT) = f.($1,0); consider f0 be Function of NAT,ExtREAL such that A1: for n be Element of NAT holds f0.n = F0(n) from FUNCT_2:sch 4; deffunc F(Element of ExtREAL,Nat,Nat) = $1 + f.($2,$3+1); consider IT be Function of [:NAT,NAT:],ExtREAL such that A2: for a be Element of NAT holds IT.(a,0) = f0.a & for n be Nat holds IT.(a,n+1) = F(IT.(a,n),a,n) from DBLSEQ_2:sch 1; take IT; hereby let n,m be Nat; A3: n in NAT & m in NAT by ORDINAL1:def 12; then IT.(n,0) = f0.n by A2; hence IT.(n,0) = f.(n,0) & IT.(n,m+1) = IT.(n,m) + f.(n,m+1) by A1,A2,A3; end; end; uniqueness proof let f1,f2 be Function of [:NAT,NAT:],ExtREAL; assume that A1: for n,m be natural number holds f1.(n,0) = f.(n,0) & f1.(n,m+1) = f1.(n,m) + f.(n,m+1) and A2: for n,m be natural number holds f2.(n,0) = f.(n,0) & f2.(n,m+1) = f2.(n,m) + f.(n,m+1); A3:dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] by FUNCT_2:def 1; for n,m be object st n in NAT & m in NAT holds f1.(n,m) = f2.(n,m) proof let n,m be object; assume n in NAT & m in NAT; then reconsider n1 = n, m1 = m as Element of NAT; defpred P[Nat] means f1.(n1,$1) = f2.(n1,$1); f1.(n1,0) = f.(n1,0) by A1; then A4: P[0] by A2; A5: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A6: P[k]; f1.(n1,k+1) = f1.(n1,k) + f.(n1,k+1) by A1; hence f1.(n1,k+1) = f2.(n1,k+1) by A2,A6; end; for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); then P[m1]; hence f1.(n,m) = f2.(n,m); end; hence thesis by A3,FUNCT_3:6; end; end; definition let f be Function of [:NAT,NAT:],ExtREAL; func Partial_Sums_in_cod1 f -> Function of [:NAT,NAT:],ExtREAL means :DefRSM: for n,m be Nat holds it.(0,m) = f.(0,m) & it.(n+1,m) = it.(n,m) + f.(n+1,m); existence proof deffunc F0(Element of NAT) = f.(0,$1); consider f0 be Function of NAT,ExtREAL such that A1: for n be Element of NAT holds f0.n = F0(n) from FUNCT_2:sch 4; deffunc F(Element of ExtREAL, Nat, Nat) = $1 + f.($3+1,$2); consider IT be Function of [:NAT,NAT:],ExtREAL such that A2: for a be Element of NAT holds IT.(0,a) = f0.a & for n be Nat holds IT.(n+1,a) = F(IT.(n,a),a,n) from DBLSEQ_2:sch 3; take IT; hereby let n,m be Nat; A3: n in NAT & m in NAT by ORDINAL1:def 12; then IT.(0,m) = f0.m by A2; hence IT.(0,m) = f.(0,m) & IT.(n+1,m) = IT.(n,m) + f.(n+1,m) by A1,A2,A3; end; end; uniqueness proof let f1,f2 be Function of [:NAT,NAT:],ExtREAL; assume that A1: for n,m be natural number holds f1.(0,m) = f.(0,m) & f1.(n+1,m) = f1.(n,m) + f.(n+1,m) and A2: for n,m be natural number holds f2.(0,m) = f.(0,m) & f2.(n+1,m) = f2.(n,m) + f.(n+1,m); A3:dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] by FUNCT_2:def 1; for n,m be object st n in NAT & m in NAT holds f1.(n,m) = f2.(n,m) proof let n,m be object; assume n in NAT & m in NAT; then reconsider n1 = n, m1 = m as Element of NAT; defpred P[Nat] means f1.($1,m1) = f2.($1,m1); f1.(0,m1) = f.(0,m1) by A1; then A4: P[0] by A2; A5: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A6: P[k]; f1.(k+1,m1) = f1.(k,m1) + f.(k+1,m1) by A1; hence f1.(k+1,m1) = f2.(k+1,m1) by A2,A6; end; for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); then P[n1]; hence f1.(n,m) = f2.(n,m); end; hence thesis by A3,FUNCT_3:6; end; end; registration let f be without-infty Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod2 f -> without-infty; correctness proof for x be object holds -infty < (Partial_Sums_in_cod2 f).x proof let x be object; per cases; suppose x in dom (Partial_Sums_in_cod2 f); then consider n,m be object such that A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A1; defpred P[Nat] means (Partial_Sums_in_cod2 f).(n,$1) > -infty; (Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then A2: P[0] by MESFUNC5:def 5; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; A5: f.(n,k+1) > -infty by MESFUNC5:def 5; (Partial_Sums_in_cod2 f).(n,k+1) = (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM; hence P[k+1] by A4,A5,XXREAL_3:17,XXREAL_0:6; end; for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then P[m]; hence -infty < (Partial_Sums_in_cod2 f).x by A1; end; suppose not x in dom (Partial_Sums_in_cod2 f); hence -infty < (Partial_Sums_in_cod2 f).x by FUNCT_1:def 2; end; end; hence (Partial_Sums_in_cod2 f) is without-infty by MESFUNC5:def 5; end; end; registration let f be without+infty Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod2 f -> without+infty; correctness proof for x be object holds +infty > (Partial_Sums_in_cod2 f).x proof let x be object; per cases; suppose x in dom (Partial_Sums_in_cod2 f); then consider n,m be object such that A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A1; defpred P[Nat] means (Partial_Sums_in_cod2 f).(n,$1) < +infty; (Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then A2: P[0] by MESFUNC5:def 6; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; A5: f.(n,k+1) < +infty by MESFUNC5:def 6; (Partial_Sums_in_cod2 f).(n,k+1) = (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM; hence P[k+1] by A4,A5,XXREAL_3:16,XXREAL_0:4; end; for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then P[m]; hence +infty > (Partial_Sums_in_cod2 f).x by A1; end; suppose not x in dom (Partial_Sums_in_cod2 f); hence +infty > (Partial_Sums_in_cod2 f).x by FUNCT_1:def 2; end; end; hence (Partial_Sums_in_cod2 f) is without+infty by MESFUNC5:def 6; end; end; registration let f be nonnegative Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod2 f -> nonnegative for Function of [:NAT,NAT:],ExtREAL; correctness proof for z be object st z in dom (Partial_Sums_in_cod2 f) holds 0. <= (Partial_Sums_in_cod2 f).z proof let z be object; assume z in dom(Partial_Sums_in_cod2 f); then consider n,m be object such that A1: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A1; defpred P[Nat] means (Partial_Sums_in_cod2 f).(n,$1) >= 0; (Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then A2: P[0] by SUPINF_2:51; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; A5: f.(n,k+1) >= 0 by SUPINF_2:51; (Partial_Sums_in_cod2 f).(n,k+1) = (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM; hence (Partial_Sums_in_cod2 f).(n,k+1) >= 0 by A5,A4; end; for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then (Partial_Sums_in_cod2 f).(n,m) >= 0; hence 0. <= (Partial_Sums_in_cod2 f).z by A1; end; hence thesis by SUPINF_2:52; end; end; registration let f be nonpositive Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod2 f -> nonpositive for Function of [:NAT,NAT:],ExtREAL; correctness proof for z be set st z in dom (Partial_Sums_in_cod2 f) holds 0. >= (Partial_Sums_in_cod2 f).z proof let z be set; assume z in dom(Partial_Sums_in_cod2 f); then consider n,m be object such that A1: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A1; defpred P[Nat] means (Partial_Sums_in_cod2 f).(n,$1) <= 0; (Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then A2: P[0] by MESFUNC5:8; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; A5: f.(n,k+1) <= 0 by MESFUNC5:8; (Partial_Sums_in_cod2 f).(n,k+1) = (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM; hence (Partial_Sums_in_cod2 f).(n,k+1) <= 0 by A5,A4; end; for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then (Partial_Sums_in_cod2 f).(n,m) <= 0; hence 0. >= (Partial_Sums_in_cod2 f).z by A1; end; hence thesis by MESFUNC5:9; end; end; registration let f be without-infty Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod1 f -> without-infty; correctness proof for x be object holds -infty < (Partial_Sums_in_cod1 f).x proof let x be object; per cases; suppose x in dom Partial_Sums_in_cod1 f; then consider n,m be object such that A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A1; defpred P[Nat] means (Partial_Sums_in_cod1 f).($1,m) > -infty; (Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM; then A2: P[0] by MESFUNC5:def 5; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; A5: f.(k+1,m) > -infty by MESFUNC5:def 5; (Partial_Sums_in_cod1 f).(k+1,m) = (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM; hence P[k+1] by A4,A5,XXREAL_3:17,XXREAL_0:6; end; for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then P[n]; hence -infty < (Partial_Sums_in_cod1 f).x by A1; end; suppose not x in dom (Partial_Sums_in_cod1 f); hence -infty < (Partial_Sums_in_cod1 f).x by FUNCT_1:def 2; end; end; hence Partial_Sums_in_cod1 f is without-infty by MESFUNC5:def 5; end; end; registration let f be without+infty Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod1 f -> without+infty; correctness proof for x be object holds +infty > (Partial_Sums_in_cod1 f).x proof let x be object; per cases; suppose x in dom (Partial_Sums_in_cod1 f); then consider n,m be object such that A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A1; defpred P[Nat] means (Partial_Sums_in_cod1 f).($1,m) < +infty; (Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM; then A2: P[0] by MESFUNC5:def 6; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; A5: f.(k+1,m) < +infty by MESFUNC5:def 6; (Partial_Sums_in_cod1 f).(k+1,m) = (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM; hence P[k+1] by A4,A5,XXREAL_3:16,XXREAL_0:4; end; for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then P[n]; hence +infty > (Partial_Sums_in_cod1 f).x by A1; end; suppose not x in dom (Partial_Sums_in_cod1 f); hence +infty > (Partial_Sums_in_cod1 f).x by FUNCT_1:def 2; end; end; hence (Partial_Sums_in_cod1 f) is without+infty by MESFUNC5:def 6; end; end; registration let f be nonnegative Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod1 f -> nonnegative for Function of [:NAT,NAT:],ExtREAL; correctness proof for z be object st z in dom (Partial_Sums_in_cod1 f) holds 0. <= (Partial_Sums_in_cod1 f).z proof let z be object; assume z in dom(Partial_Sums_in_cod1 f); then consider m,n be object such that A1: m in NAT & n in NAT & z = [m,n] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A1; defpred P[Nat] means (Partial_Sums_in_cod1 f).($1,n) >= 0; (Partial_Sums_in_cod1 f).(0,n) = f.(0,n) by DefRSM; then A2: P[0] by SUPINF_2:51; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; A5: f.(k+1,n) >= 0 by SUPINF_2:51; (Partial_Sums_in_cod1 f).(k+1,n) = (Partial_Sums_in_cod1 f).(k,n) + f.(k+1,n) by DefRSM; hence (Partial_Sums_in_cod1 f).(k+1,n) >= 0 by A5,A4; end; for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then (Partial_Sums_in_cod1 f).(m,n) >= 0; hence 0. <= (Partial_Sums_in_cod1 f).z by A1; end; hence thesis by SUPINF_2:52; end; end; registration let f be nonpositive Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod1 f -> nonpositive for Function of [:NAT,NAT:],ExtREAL; correctness proof for z be set st z in dom (Partial_Sums_in_cod1 f) holds 0. >= (Partial_Sums_in_cod1 f).z proof let z be set; assume z in dom(Partial_Sums_in_cod1 f); then consider m,n be object such that A1: m in NAT & n in NAT & z = [m,n] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A1; defpred P[Nat] means (Partial_Sums_in_cod1 f).($1,n) <= 0; (Partial_Sums_in_cod1 f).(0,n) = f.(0,n) by DefRSM; then A2: P[0] by MESFUNC5:8; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; A5: f.(k+1,n) <= 0 by MESFUNC5:8; (Partial_Sums_in_cod1 f).(k+1,n) = (Partial_Sums_in_cod1 f).(k,n) + f.(k+1,n) by DefRSM; hence (Partial_Sums_in_cod1 f).(k+1,n) <= 0 by A5,A4; end; for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then (Partial_Sums_in_cod1 f).(m,n) <= 0; hence 0. >= (Partial_Sums_in_cod1 f).z by A1; end; hence thesis by MESFUNC5:9; end; end; definition let f be Function of [:NAT,NAT:],ExtREAL; func Partial_Sums f -> Function of [:NAT,NAT:],ExtREAL equals Partial_Sums_in_cod2( Partial_Sums_in_cod1 f ); correctness; end; theorem Th39: for f be Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (Partial_Sums_in_cod1 f).(n,m) = (Partial_Sums_in_cod2 f@).(m,n) & (Partial_Sums_in_cod2 f).(n,m) = (Partial_Sums_in_cod1 f@).(m,n) proof let f be Function of [:NAT,NAT:],ExtREAL; let n,m be Nat; reconsider n1=n, m1=m as Element of NAT by ORDINAL1:def 12; defpred P1[Nat] means (Partial_Sums_in_cod1 f).($1,m) = (Partial_Sums_in_cod2 f@).(m,$1); (Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM .= (f@).(m1,0) by DBLSEQ_2:def 2; then A2:P1[0] by DefCSM; A3:for k be Nat st P1[k] holds P1[k+1] proof let k be Nat; assume A4: P1[k]; (Partial_Sums_in_cod1 f).(k+1,m) = (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM .= (Partial_Sums_in_cod2 f@).(m,k) + f@.(m1,k+1) by A4,DBLSEQ_2:def 2; hence P1[k+1] by DefCSM; end; for k be Nat holds P1[k] from NAT_1:sch 2(A2,A3); hence (Partial_Sums_in_cod1 f).(n,m) = (Partial_Sums_in_cod2 f@).(m,n); defpred P2[Nat] means (Partial_Sums_in_cod2 f).(n,$1) = (Partial_Sums_in_cod1 f@).($1,n); (Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM .= (f@).(0,n1) by DBLSEQ_2:def 2; then A5:P2[0] by DefRSM; A6:for k be Nat st P2[k] holds P2[k+1] proof let k be Nat; assume A7: P2[k]; (Partial_Sums_in_cod2 f).(n,k+1) = (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM .= (Partial_Sums_in_cod1 f@).(k,n) + f@.(k+1,n1) by A7,DBLSEQ_2:def 2; hence P2[k+1] by DefRSM; end; for k be Nat holds P2[k] from NAT_1:sch 2(A5,A6); hence (Partial_Sums_in_cod2 f).(n,m) = (Partial_Sums_in_cod1 f@).(m,n); end; theorem Th40: for f be Function of [:NAT,NAT:],ExtREAL holds (Partial_Sums_in_cod1 f)@ = Partial_Sums_in_cod2 f@ & (Partial_Sums_in_cod2 f)@ = Partial_Sums_in_cod1 f@ proof let f be Function of [:NAT,NAT:],ExtREAL; now let z be Element of [:NAT,NAT:]; consider n,m be object such that A1: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A1; (Partial_Sums_in_cod2 f@).z = (Partial_Sums_in_cod2 f@).(n,m) by A1 .= (Partial_Sums_in_cod1 f).(m,n) by Th39 .= (Partial_Sums_in_cod1 f)@.(n,m) by DBLSEQ_2:def 2; hence (Partial_Sums_in_cod2 f@).z = (Partial_Sums_in_cod1 f)@.z by A1; end; hence (Partial_Sums_in_cod1 f)@ = Partial_Sums_in_cod2 f@ by FUNCT_2:def 8; now let z be Element of [:NAT,NAT:]; consider n,m be object such that A2: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A2; (Partial_Sums_in_cod1 f@).z = (Partial_Sums_in_cod1 f@).(n,m) by A2 .= (Partial_Sums_in_cod2 f).(m,n) by Th39 .= (Partial_Sums_in_cod2 f)@.(n,m) by DBLSEQ_2:def 2; hence (Partial_Sums_in_cod1 f@).z = (Partial_Sums_in_cod2 f)@.z by A2; end; hence (Partial_Sums_in_cod2 f)@ = Partial_Sums_in_cod1 f@ by FUNCT_2:def 8; end; theorem for f be Function of [:NAT,NAT:],ExtREAL, g be ext-real-valued Function, n be Nat st (for k be Nat holds (Partial_Sums_in_cod1 f).(n,k) = g.k) holds (for k be Nat holds (Partial_Sums f).(n,k) = (Partial_Sums g).k) & (lim_in_cod2(Partial_Sums f)).n = Sum g proof let f be Function of [:NAT,NAT:],ExtREAL, g be ext-real-valued Function, n be Nat; assume A1: for k be Nat holds (Partial_Sums_in_cod1 f).(n,k) = g.k; A4:now let k be Nat; defpred P[Nat] means (Partial_Sums f).(n,$1) = (Partial_Sums g).$1; (Partial_Sums f).(n,0) = (Partial_Sums_in_cod1 f).(n,0) by DefCSM .= g.0 by A1; then A2: P[0] by MESFUNC9:def 1; A3: for m be Nat st P[m] holds P[m+1] proof let m be Nat; assume A4: P[m]; (Partial_Sums f).(n,m+1) = (Partial_Sums_in_cod2(Partial_Sums_in_cod1 f)).(n,m) + (Partial_Sums_in_cod1 f).(n,m+1) by DefCSM .= (Partial_Sums g).m + g.(m+1) by A1,A4; hence P[m+1] by MESFUNC9:def 1; end; for m be Nat holds P[m] from NAT_1:sch 2(A2,A3); hence (Partial_Sums f).(n,k) = (Partial_Sums g).k; end; reconsider n1=n as Element of NAT by ORDINAL1:def 12; now let k be Element of NAT; ProjMap1(Partial_Sums f,n1).k = (Partial_Sums f).(n,k) by MESFUNC9:def 6; hence ProjMap1(Partial_Sums f,n1).k = (Partial_Sums g).k by A4; end; then ProjMap1(Partial_Sums f,n1) = Partial_Sums g by FUNCT_2:def 8; then (lim_in_cod2(Partial_Sums f)).n1 = lim (Partial_Sums g) by D1DEF6; hence thesis by A4,MESFUNC9:def 3; end; theorem Th42: for f be Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod2(-f) = -(Partial_Sums_in_cod2 f) & Partial_Sums_in_cod1(-f) = -(Partial_Sums_in_cod1 f) proof let f be Function of [:NAT,NAT:],ExtREAL; A1:dom(-(Partial_Sums_in_cod2 f)) = [:NAT,NAT:] & dom(-(Partial_Sums_in_cod1 f)) = [:NAT,NAT:] by FUNCT_2:def 1; A2:dom(-f) = [:NAT,NAT:] by FUNCT_2:def 1; for z be Element of [:NAT,NAT:] holds (-(Partial_Sums_in_cod2 f)).z = (Partial_Sums_in_cod2(-f)).z proof let z be Element of [:NAT,NAT:]; consider n,m be object such that A3: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A3; defpred P[Nat] means (Partial_Sums_in_cod2(-f)).(n,$1) = -((Partial_Sums_in_cod2 f).(n,$1)); reconsider z0 = [n,0] as Element of [:NAT,NAT:] by ZFMISC_1:87; A4: [n,0] in [:NAT,NAT:] by ZFMISC_1:87; (Partial_Sums_in_cod2(-f)).(n,0) = (-f).(n,0) by DefCSM .= -(f.(n,0)) by A4,A2,MESFUNC1:def 7; then A5: P[0] by DefCSM; A6: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A7: P[k]; A8: [n,k+1] in [:NAT,NAT:] by ZFMISC_1:87; thus (Partial_Sums_in_cod2 -f).(n,k+1) = (Partial_Sums_in_cod2 -f).(n,k) + (-f).(n,k+1) by DefCSM .= -((Partial_Sums_in_cod2 f).(n,k)) -(f.(n,k+1)) by A7,A8,A2,MESFUNC1:def 7 .= -((Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1)) by XXREAL_3:25 .= -( (Partial_Sums_in_cod2 f).(n,k+1) ) by DefCSM; end; for k be Nat holds P[k] from NAT_1:sch 2(A5,A6); then (Partial_Sums_in_cod2(-f)).(n,m) = -((Partial_Sums_in_cod2 f).(n,m)); hence thesis by A3,A1,MESFUNC1:def 7; end; hence Partial_Sums_in_cod2(-f) = -(Partial_Sums_in_cod2 f) by FUNCT_2:def 8; for z be Element of [:NAT,NAT:] holds (-(Partial_Sums_in_cod1 f)).z = (Partial_Sums_in_cod1(-f)).z proof let z be Element of [:NAT,NAT:]; consider n,m be object such that A3: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2; reconsider n,m as Element of NAT by A3; defpred P[Nat] means (Partial_Sums_in_cod1(-f)).($1,m) = -((Partial_Sums_in_cod1 f).($1,m)); reconsider z0 = [0,m] as Element of [:NAT,NAT:] by ZFMISC_1:87; A4: [0,m] in [:NAT,NAT:] by ZFMISC_1:87; (Partial_Sums_in_cod1(-f)).(0,m) = (-f).(0,m) by DefRSM .= -(f.(0,m)) by A4,A2,MESFUNC1:def 7; then A5: P[0] by DefRSM; A6: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A7: P[k]; A8: [k+1,m] in [:NAT,NAT:] by ZFMISC_1:87; thus (Partial_Sums_in_cod1 -f).(k+1,m) = (Partial_Sums_in_cod1 -f).(k,m) + (-f).(k+1,m) by DefRSM .= -((Partial_Sums_in_cod1 f).(k,m)) -(f.(k+1,m)) by A7,A8,A2,MESFUNC1:def 7 .= -((Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m)) by XXREAL_3:25 .= -( (Partial_Sums_in_cod1 f).(k+1,m) ) by DefRSM; end; for k be Nat holds P[k] from NAT_1:sch 2(A5,A6); then (Partial_Sums_in_cod1(-f)).(n,m) = -((Partial_Sums_in_cod1 f).(n,m)); hence thesis by A3,A1,MESFUNC1:def 7; end; hence Partial_Sums_in_cod1(-f) = -(Partial_Sums_in_cod1 f) by FUNCT_2:def 8; end; theorem Th43: for f be Function of [:NAT,NAT:],ExtREAL, m,n be Element of NAT holds (Partial_Sums_in_cod1 f).(m,n) = Partial_Sums(ProjMap2(f,n)).m & (Partial_Sums_in_cod2 f).(m,n) = Partial_Sums(ProjMap1(f,m)).n proof let f be Function of [:NAT,NAT:],ExtREAL; let m,n be Element of NAT; defpred P[Nat] means (Partial_Sums_in_cod1 f).($1,n) = Partial_Sums(ProjMap2(f,n)).$1; Partial_Sums(ProjMap2(f,n)).0 = (ProjMap2(f,n)).0 by MESFUNC9:def 1 .= f.(0,n) by MESFUNC9:def 7; then a1:P[0] by DefRSM; a2:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; then (Partial_Sums_in_cod1 f).(k+1,n) = Partial_Sums(ProjMap2(f,n)).k + f.(k+1,n) by DefRSM .= Partial_Sums(ProjMap2(f,n)).k + (ProjMap2(f,n)).(k+1) by MESFUNC9:def 7; hence P[k+1] by MESFUNC9:def 1; end; for k be Nat holds P[k] from NAT_1:sch 2(a1,a2); hence (Partial_Sums_in_cod1 f).(m,n) = Partial_Sums(ProjMap2(f,n)).m; defpred Q[Nat] means (Partial_Sums_in_cod2 f).(m,$1) = Partial_Sums(ProjMap1(f,m)).$1; Partial_Sums(ProjMap1(f,m)).0 = (ProjMap1(f,m)).0 by MESFUNC9:def 1 .= f.(m,0) by MESFUNC9:def 6; then a3:Q[0] by DefCSM; a4:for k be Nat st Q[k] holds Q[k+1] proof let k be Nat; assume Q[k]; then (Partial_Sums_in_cod2 f).(m,k+1) = Partial_Sums(ProjMap1(f,m)).k + f.(m,k+1) by DefCSM .= Partial_Sums(ProjMap1(f,m)).k + (ProjMap1(f,m)).(k+1) by MESFUNC9:def 6; hence Q[k+1] by MESFUNC9:def 1; end; for k be Nat holds Q[k] from NAT_1:sch 2(a3,a4); hence thesis; end; theorem Th44: for f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod2(f1+f2) = Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 f2 & Partial_Sums_in_cod1(f1+f2) = Partial_Sums_in_cod1 f1 + Partial_Sums_in_cod1 f2 proof let f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL; set CS1 = Partial_Sums_in_cod2 f1; set CS2 = Partial_Sums_in_cod2 f2; set CS12 = Partial_Sums_in_cod2(f1+f2); set RS1 = Partial_Sums_in_cod1 f1; set RS2 = Partial_Sums_in_cod1 f2; set RS12 = Partial_Sums_in_cod1(f1+f2); now let n be Element of NAT, m be Element of NAT; defpred C[Nat] means CS12.(n,$1) = CS1.(n,$1) + CS2.(n,$1); CS12.(n,0) = (f1+f2).(n,0) by DefCSM .= f1.(n,0) + f2.(n,0) by Th11 .= CS1.(n,0) + f2.(n,0) by DefCSM; then a1: C[0] by DefCSM; a2: for k be Nat st C[k] holds C[k+1] proof let k be Nat; assume a3: C[k]; X1: CS1.(n,k) <> -infty & CS2.(n,k) <> -infty & f1.(n,k+1) <> -infty & f2.(n,k+1) <> -infty & (f1+f2).(n,k+1) <> -infty by MESFUNC5:def 5; then X2: CS2.(n,k) + f2.(n,k+1) <> -infty by XXREAL_3:17; CS12.(n,k+1) = CS12.(n,k) + (f1+f2).(n,k+1) by DefCSM .= CS1.(n,k) + ( (f1+f2).(n,k+1) + CS2.(n,k) ) by a3,X1,XXREAL_3:29 .= CS1.(n,k) + ( f1.(n,k+1) + f2.(n,k+1) + CS2.(n,k) ) by Th11 .= CS1.(n,k) + ( f1.(n,k+1) + ( CS2.(n,k) + f2.(n,k+1) ) ) by X1,XXREAL_3:29 .= CS1.(n,k) + f1.(n,k+1) + ( CS2.(n,k) + f2.(n,k+1) ) by X1,X2,XXREAL_3:29 .= CS1.(n,k+1) + ( CS2.(n,k) + f2.(n,k+1) ) by DefCSM; hence C[k+1] by DefCSM; end; for k be Nat holds C[k] from NAT_1:sch 2(a1,a2); then C[m]; hence CS12.(n,m) = (CS1+CS2).(n,m) by Th11; end; hence CS12 = CS1 + CS2 by BINOP_1:2; now let n,m be Element of NAT; defpred R[Nat] means RS12.($1,m) = RS1.($1,m) + RS2.($1,m); RS12.(0,m) = (f1+f2).(0,m) by DefRSM .= f1.(0,m) + f2.(0,m) by Th11 .= RS1.(0,m) + f2.(0,m) by DefRSM; then a4: R[0] by DefRSM; a5: for k be Nat st R[k] holds R[k+1] proof let k be Nat; assume a6: R[k]; X3: RS1.(k,m) <> -infty & RS2.(k,m) <> -infty & f1.(k+1,m) <> -infty & f2.(k+1,m) <> -infty & (f1+f2).(k+1,m) <> -infty by MESFUNC5:def 5; then X4: RS2.(k,m) + f2.(k+1,m) <> -infty by XXREAL_3:17; RS12.(k+1,m) = RS12.(k,m) + (f1+f2).(k+1,m) by DefRSM .= RS1.(k,m) + ( (f1+f2).(k+1,m) + RS2.(k,m) ) by a6,X3,XXREAL_3:29 .= RS1.(k,m) + ( f1.(k+1,m) + f2.(k+1,m) + RS2.(k,m) ) by Th11 .= RS1.(k,m) + ( f1.(k+1,m) + ( RS2.(k,m) + f2.(k+1,m) ) ) by X3,XXREAL_3:29 .= RS1.(k,m) + f1.(k+1,m) + ( RS2.(k,m) + f2.(k+1,m) ) by X3,X4,XXREAL_3:29 .= RS1.(k+1,m) + (RS2.(k,m) + f2.(k+1,m)) by DefRSM; hence R[k+1] by DefRSM; end; for k be Nat holds R[k] from NAT_1:sch 2(a4,a5); then R[n]; hence RS12.(n,m) = (RS1+RS2).(n,m) by Th11; end; hence RS12 = RS1 + RS2 by BINOP_1:2; end; theorem Th45: for f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod2(f1+f2) = Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 f2 & Partial_Sums_in_cod1(f1+f2) = Partial_Sums_in_cod1 f1 + Partial_Sums_in_cod1 f2 proof let f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL; reconsider F1=-f1, F2=-f2 as without-infty Function of [:NAT,NAT:],ExtREAL; F1+F2 = -f1 -f2 by Th10 .= -(f1+f2) by Th9; then A1:-(F1+F2) = f1+f2 by Th2; then Partial_Sums_in_cod2(f1+f2) = -(Partial_Sums_in_cod2(F1+F2)) by Th42 .= -(Partial_Sums_in_cod2 F1 + Partial_Sums_in_cod2 F2) by Th44 .= -( -(Partial_Sums_in_cod2 f1) + Partial_Sums_in_cod2 F2 ) by Th42 .= -( -(Partial_Sums_in_cod2 f1) + -(Partial_Sums_in_cod2 f2) ) by Th42 .= -(-(Partial_Sums_in_cod2 f1)) -(-(Partial_Sums_in_cod2 f2)) by Th8 .= Partial_Sums_in_cod2 f1 -(-(Partial_Sums_in_cod2 f2)) by Th2 .= Partial_Sums_in_cod2 f1 + (-(-(Partial_Sums_in_cod2 f2))) by Th10; hence Partial_Sums_in_cod2(f1+f2) = Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 f2 by Th2; Partial_Sums_in_cod1(f1+f2) = -(Partial_Sums_in_cod1(F1+F2)) by A1,Th42 .= -(Partial_Sums_in_cod1 F1 + Partial_Sums_in_cod1 F2) by Th44 .= -( -(Partial_Sums_in_cod1 f1) + Partial_Sums_in_cod1 F2 ) by Th42 .= -( -(Partial_Sums_in_cod1 f1) + -(Partial_Sums_in_cod1 f2) ) by Th42 .= -(-(Partial_Sums_in_cod1 f1)) -(-(Partial_Sums_in_cod1 f2)) by Th8 .= Partial_Sums_in_cod1 f1 -(-(Partial_Sums_in_cod1 f2)) by Th2 .= Partial_Sums_in_cod1 f1 + (-(-(Partial_Sums_in_cod1 f2))) by Th10; hence thesis by Th2; end; theorem Th46: for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod2(f1-f2) = Partial_Sums_in_cod2 f1 - Partial_Sums_in_cod2 f2 & Partial_Sums_in_cod1(f1-f2) = Partial_Sums_in_cod1 f1 - Partial_Sums_in_cod1 f2 & Partial_Sums_in_cod2(f2-f1) = Partial_Sums_in_cod2 f2 - Partial_Sums_in_cod2 f1 & Partial_Sums_in_cod1(f2-f1) = Partial_Sums_in_cod1 f2 - Partial_Sums_in_cod1 f1 proof let f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be without+infty Function of [:NAT,NAT:],ExtREAL; Partial_Sums_in_cod2(f1-f2) = Partial_Sums_in_cod2(f1+(-f2)) by Th10 .= Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 (-f2) by Th44 .= Partial_Sums_in_cod2 f1 + -(Partial_Sums_in_cod2 f2) by Th42; hence Partial_Sums_in_cod2(f1-f2) = Partial_Sums_in_cod2 f1 - Partial_Sums_in_cod2 f2 by Th10; Partial_Sums_in_cod1(f1-f2) = Partial_Sums_in_cod1(f1+(-f2)) by Th10 .= Partial_Sums_in_cod1 f1 + Partial_Sums_in_cod1 (-f2) by Th44 .= Partial_Sums_in_cod1 f1 + -(Partial_Sums_in_cod1 f2) by Th42; hence Partial_Sums_in_cod1(f1-f2) = Partial_Sums_in_cod1 f1 - Partial_Sums_in_cod1 f2 by Th10; Partial_Sums_in_cod2(f2-f1) = Partial_Sums_in_cod2(f2+(-f1)) by Th10 .= Partial_Sums_in_cod2 f2 + Partial_Sums_in_cod2 (-f1) by Th45 .= Partial_Sums_in_cod2 f2 + -(Partial_Sums_in_cod2 f1) by Th42; hence Partial_Sums_in_cod2(f2-f1) = Partial_Sums_in_cod2 f2 - Partial_Sums_in_cod2 f1 by Th10; Partial_Sums_in_cod1(f2-f1) = Partial_Sums_in_cod1(f2+(-f1)) by Th10 .= Partial_Sums_in_cod1 f2 + Partial_Sums_in_cod1 (-f1) by Th45 .= Partial_Sums_in_cod1 f2 + -(Partial_Sums_in_cod1 f1) by Th42; hence Partial_Sums_in_cod1(f2-f1) = Partial_Sums_in_cod1 f2 - Partial_Sums_in_cod1 f1 by Th10; end; theorem Th47: for f be without-infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (Partial_Sums f).(n+1,m) = (Partial_Sums_in_cod2 f).(n+1,m) + (Partial_Sums f).(n,m) & (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m+1) = (Partial_Sums_in_cod1 f).(n,m+1) + (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m) proof let f be without-infty Function of [:NAT,NAT:],ExtREAL; let n,m be Nat; set RPS = Partial_Sums f; set CPS = Partial_Sums_in_cod1(Partial_Sums_in_cod2 f); set ROW = Partial_Sums_in_cod1 f; set COL = Partial_Sums_in_cod2 f; defpred P[Nat] means RPS.(n+1,$1) = COL.(n+1,$1) + RPS.(n,$1); a1:RPS.(n,0) = ROW.(n,0) by DefCSM; RPS.(n+1,0) = ROW.(n+1,0) by DefCSM .= ROW.(n,0) + f.(n+1,0) by DefRSM; then a3:P[0] by a1,DefCSM; a4:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A5: P[k]; a6: COL.(n+1,k+1) = COL.(n+1,k) + f.(n+1,k+1) by DefCSM; X1: COL.(n+1,k) <> -infty & f.(n+1,k+1) <> -infty & RPS.(n,k) <> -infty & ROW.(n,k+1) <> -infty & RPS.(n+1,k) <> -infty by MESFUNC5:def 5; then X2: COL.(n+1,k) + f.(n+1,k+1) <> -infty by XXREAL_3:17; RPS.(n,k+1) = RPS.(n,k) + ROW.(n,k+1) by DefCSM; then COL.(n+1,k+1) + RPS.(n,k+1) = COL.(n+1,k) + f.(n+1,k+1) + RPS.(n,k) + ROW.(n,k+1) by a6,X1,X2,XXREAL_3:29 .= COL.(n+1,k) + RPS.(n,k) + f.(n+1,k+1) + ROW.(n,k+1) by X1,XXREAL_3:29 .= RPS.(n+1,k) + ( f.(n+1,k+1) + ROW.(n,k+1) ) by A5,X1,XXREAL_3:29 .= RPS.(n+1,k) + ROW.(n+1,k+1) by DefRSM; hence P[k+1] by DefCSM; end; for k be Nat holds P[k] from NAT_1:sch 2(a3,a4); hence RPS.(n+1,m) = COL.(n+1,m) + RPS.(n,m); defpred Q[Nat] means CPS.($1,m+1) = ROW.($1,m+1) + CPS.($1,m); b1:CPS.(0,m) = COL.(0,m) by DefRSM; CPS.(0,m+1) = COL.(0,m+1) by DefRSM .= COL.(0,m) + f.(0,m+1) by DefCSM; then b3:Q[0] by b1,DefRSM; b4:for k be Nat st Q[k] holds Q[k+1] proof let k be Nat; assume B5: Q[k]; b6: ROW.(k+1,m+1) = ROW.(k,m+1) + f.(k+1,m+1) by DefRSM; X3: ROW.(k,m+1) <> -infty & f.(k+1,m+1) <> -infty & CPS.(k,m) <> -infty & COL.(k+1,m) <> -infty & CPS.(k,m+1) <> -infty by MESFUNC5:def 5; then X4: ROW.(k,m+1) + f.(k+1,m+1) <> -infty by XXREAL_3:17; CPS.(k+1,m) = CPS.(k,m) + COL.(k+1,m) by DefRSM; then ROW.(k+1,m+1) + CPS.(k+1,m) = ROW.(k,m+1) + f.(k+1,m+1) + CPS.(k,m) + COL.(k+1,m) by b6,X3,X4,XXREAL_3:29 .= ROW.(k,m+1) + CPS.(k,m) + f.(k+1,m+1) + COL.(k+1,m) by X3,XXREAL_3:29 .= CPS.(k,m+1) + ( f.(k+1,m+1) + COL.(k+1,m) ) by B5,X3,XXREAL_3:29 .= CPS.(k,m+1) + COL.(k+1,m+1) by DefCSM; hence Q[k+1] by DefRSM; end; for k be Nat holds Q[k] from NAT_1:sch 2(b3,b4); hence thesis; end; theorem for f be without+infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (Partial_Sums f).(n+1,m) = (Partial_Sums_in_cod2 f).(n+1,m) + (Partial_Sums f).(n,m) & (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m+1) = (Partial_Sums_in_cod1 f).(n,m+1) + (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m) proof let f be without+infty Function of [:NAT,NAT:],ExtREAL; let n,m be Nat; reconsider g = -f as without-infty Function of [:NAT,NAT:],ExtREAL; A2:dom(-(Partial_Sums_in_cod2(Partial_Sums_in_cod1 g))) = [:NAT,NAT:] & dom(-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g))) = [:NAT,NAT:] by FUNCT_2:def 1; A4:dom(-(Partial_Sums_in_cod2 g)) = [:NAT,NAT:] & dom(-(Partial_Sums_in_cod1 g)) = [:NAT,NAT:] by FUNCT_2:def 1; A5:dom(-(Partial_Sums g)) = [:NAT,NAT:] by FUNCT_2:def 1; n in NAT & m in NAT by ORDINAL1:def 12; then A3:[n+1,m] in [:NAT,NAT:] & [n,m] in [:NAT,NAT:] & [n,m+1] in [:NAT,NAT:] by ZFMISC_1:87; A1:Partial_Sums f = Partial_Sums_in_cod2(Partial_Sums_in_cod1 (-(g))) by Th2 .= Partial_Sums_in_cod2(-(Partial_Sums_in_cod1 g)) by Th42 .= -(Partial_Sums g) by Th42; thus (Partial_Sums f).(n+1,m) = -( (Partial_Sums_in_cod2(Partial_Sums_in_cod1 g)).(n+1,m) ) by A1,A2,A3,MESFUNC1:def 7 .= -( (Partial_Sums_in_cod2 g).(n+1,m) + (Partial_Sums g).(n,m) ) by Th47 .= - (Partial_Sums_in_cod2 g).(n+1,m) - (Partial_Sums g).(n,m) by XXREAL_3:25 .= (-(Partial_Sums_in_cod2 g)).(n+1,m) + -(Partial_Sums g).(n,m) by A3,A4,MESFUNC1:def 7 .= (Partial_Sums_in_cod2(-g)).(n+1,m) + -(Partial_Sums g).(n,m) by Th42 .= (Partial_Sums_in_cod2 f).(n+1,m) + -(Partial_Sums g).(n,m) by Th2 .= (Partial_Sums_in_cod2 f).(n+1,m) + (Partial_Sums f).(n,m) by A1,A3,A5,MESFUNC1:def 7; thus (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m+1) = (Partial_Sums_in_cod1( (Partial_Sums_in_cod2(-g)) )).(n,m+1) by Th2 .= (Partial_Sums_in_cod1( -(Partial_Sums_in_cod2 g) )).(n,m+1) by Th42 .= ( -(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)) ).(n,m+1) by Th42 .= -( (Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)).(n,m+1) ) by A3,A2,MESFUNC1:def 7 .= -( (Partial_Sums_in_cod1 g).(n,m+1) +(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)).(n,m) ) by Th47 .= -(Partial_Sums_in_cod1 g).(n,m+1) -(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)).(n,m) by XXREAL_3:25 .= (-(Partial_Sums_in_cod1 g)).(n,m+1) -(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)).(n,m) by A4,A3,MESFUNC1:def 7 .= (-(Partial_Sums_in_cod1 g)).(n,m+1) + (-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g))).(n,m) by A3,A2,MESFUNC1:def 7 .= (Partial_Sums_in_cod1(-g)).(n,m+1) + (-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g))).(n,m) by Th42 .= (Partial_Sums_in_cod1 f).(n,m+1) + (-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g))).(n,m) by Th2 .= (Partial_Sums_in_cod1 f).(n,m+1) + ((Partial_Sums_in_cod1-(Partial_Sums_in_cod2 g))).(n,m) by Th42 .= (Partial_Sums_in_cod1 f).(n,m+1) + ((Partial_Sums_in_cod1(Partial_Sums_in_cod2(-g)))).(n,m) by Th42 .= (Partial_Sums_in_cod1 f).(n,m+1) + ((Partial_Sums_in_cod1(Partial_Sums_in_cod2 f))).(n,m) by Th2; end; Lm7: for f be without-infty Function of [:NAT,NAT:],ExtREAL, m,n be Nat holds (Partial_Sums f).(m,n) = (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(m,n) proof let f be without-infty Function of [:NAT,NAT:],ExtREAL, m,n be Nat; defpred P1[Nat] means for m be Nat holds (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(m,$1) = (Partial_Sums f).(m,$1); defpred P2[Nat] means (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).($1,0) = (Partial_Sums f).($1,0); Y3:(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,0) = (Partial_Sums_in_cod2 f).(0,0) by DefRSM .= f.(0,0) by DefCSM; (Partial_Sums f).(0,0) = (Partial_Sums_in_cod1(f)).(0,0) by DefCSM .= f.(0,0) by DefRSM; then Y1:P2[0] by Y3; Y2:for i be Nat st P2[i] holds P2[i+1] proof let i be Nat; assume Y3: P2[i]; Y4: (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i+1,0) = (Partial_Sums_in_cod1(Partial_Sums_in_cod2(f))).(i,0) + (Partial_Sums_in_cod2(f)).(i+1,0) by DefRSM .= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,0) + f.(i+1,0) by DefCSM; (Partial_Sums f).(i+1,0) = (Partial_Sums_in_cod1 f).(i+1,0) by DefCSM .= (Partial_Sums_in_cod1 f).(i,0) + f.(i+1,0) by DefRSM .= (Partial_Sums f).(i,0) + f.(i+1,0) by DefCSM; hence P2[i+1] by Y3,Y4; end; for n be Nat holds P2[n] from NAT_1:sch 2(Y1,Y2); then X1:P1[0]; X2:for j be Nat st P1[j] holds P1[j+1] proof let j be Nat; assume Z3: P1[j]; for m be Nat holds (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(m,j+1) = (Partial_Sums f).(m,j+1) proof let n be Nat; defpred P3[Nat] means (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).($1,j+1) = (Partial_Sums f).($1,j+1); Z4: (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,j+1) = (Partial_Sums_in_cod2 f).(0,j+1) by DefRSM .= (Partial_Sums_in_cod2 f).(0,j) + f.(0,j+1) by DefCSM .= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,j) + f.(0,j+1) by DefRSM; (Partial_Sums f).(0,j+1) = (Partial_Sums f).(0,j) + (Partial_Sums_in_cod1 f).(0,j+1) by DefCSM .= (Partial_Sums f).(0,j) + f.(0,j+1) by DefRSM .= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,j) + f.(0,j+1) by Z3; then Z1: P3[0] by Z4; Z2: for i be Nat st P3[i] holds P3[i+1] proof let i be Nat; assume P3[i]; W1: (Partial_Sums f).(i,j) <> -infty & (Partial_Sums_in_cod1 f).(i,j+1) <> -infty & (Partial_Sums_in_cod2 f).(i+1,j) <> -infty & f.(i+1,j+1) <> -infty & (Partial_Sums_in_cod1 f).(i+1,j+1) <> -infty & (Partial_Sums_in_cod2 f).(i+1,j) <> -infty by MESFUNC5:def 5; then W2: (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i,j+1) <> -infty by XXREAL_3:17; Z6: (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,j) = (Partial_Sums f).(i,j) by Z3; (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i+1,j+1) = (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,j+1) + (Partial_Sums_in_cod2 f).(i+1,j+1) by DefRSM .= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i,j+1) + (Partial_Sums_in_cod2 f).(i+1,j+1) by Z6,Th47 .= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i,j+1) + ( (Partial_Sums_in_cod2 f).(i+1,j) + f.(i+1,j+1) ) by DefCSM .= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i,j+1) + f.(i+1,j+1) + (Partial_Sums_in_cod2 f).(i+1,j) by W1,W2,XXREAL_3:29 .= (Partial_Sums f).(i,j) + ( (Partial_Sums_in_cod1(f)).(i,j+1) + f.(i+1,j+1) ) + (Partial_Sums_in_cod2(f)).(i+1,j) by W1,XXREAL_3:29 .= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i+1,j+1) + (Partial_Sums_in_cod2 f).(i+1,j) by DefRSM .= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod2 f).(i+1,j) + (Partial_Sums_in_cod1 f).(i+1,j+1) by W1,XXREAL_3:29 .= (Partial_Sums f).(i+1,j) + (Partial_Sums_in_cod1 f).(i+1,j+1) by Th47; hence thesis by DefCSM; end; for n be Nat holds P3[n] from NAT_1:sch 2(Z1,Z2); hence thesis; end; hence P1[j+1]; end; for m be Nat holds P1[m] from NAT_1:sch 2(X1,X2); hence thesis; end; Lm8: for f be without-infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f = Partial_Sums_in_cod1(Partial_Sums_in_cod2 f) proof let f be without-infty Function of [:NAT,NAT:],ExtREAL; now let x be Element of [:NAT,NAT:]; consider n,m be object such that A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2; reconsider n1=n,m1=m as Nat by A1; (Partial_Sums f).(n1,m1) = (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n1,m1) by Lm7; hence (Partial_Sums f).x = (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).x by A1; end; hence thesis by FUNCT_2:63; end; Lm9: for f be without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f = Partial_Sums_in_cod1(Partial_Sums_in_cod2 f) proof let f be without+infty Function of [:NAT,NAT:],ExtREAL; reconsider g = -f as without-infty Function of [:NAT,NAT:],ExtREAL; A1:Partial_Sums f = Partial_Sums (-g) by Th2 .= Partial_Sums_in_cod2(-(Partial_Sums_in_cod1 g)) by Th42 .= -(Partial_Sums g) by Th42; Partial_Sums_in_cod1(Partial_Sums_in_cod2 f) = Partial_Sums_in_cod1(Partial_Sums_in_cod2 (-g)) by Th2 .= Partial_Sums_in_cod1(-(Partial_Sums_in_cod2 g)) by Th42 .= -(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)) by Th42; hence thesis by A1,Lm8; end; theorem for f be Function of [:NAT,NAT:],ExtREAL st f is without-infty or f is without+infty holds Partial_Sums f = Partial_Sums_in_cod1(Partial_Sums_in_cod2 f) by Lm8,Lm9; theorem for f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums(f1 + f2) = Partial_Sums f1 + Partial_Sums f2 proof let f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL; Partial_Sums(f1+f2) = Partial_Sums_in_cod2(Partial_Sums_in_cod1 f1 +Partial_Sums_in_cod1 f2) by Th44; hence thesis by Th44; end; theorem for f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums(f1 + f2) = Partial_Sums f1 + Partial_Sums f2 proof let f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL; Partial_Sums(f1+f2) = Partial_Sums_in_cod2(Partial_Sums_in_cod1 f1 +Partial_Sums_in_cod1 f2) by Th45; hence thesis by Th45; end; theorem for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums(f1 - f2) = Partial_Sums f1 - Partial_Sums f2 & Partial_Sums(f2 - f1) = Partial_Sums f2 - Partial_Sums f1 proof let f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be without+infty Function of [:NAT,NAT:],ExtREAL; Partial_Sums(f1-f2) = Partial_Sums_in_cod2(Partial_Sums_in_cod1 f1 - Partial_Sums_in_cod1 f2) by Th46; hence Partial_Sums(f1-f2) = Partial_Sums f1 - Partial_Sums f2 by Th46; Partial_Sums(f2-f1) = Partial_Sums_in_cod2(Partial_Sums_in_cod1 f2 - Partial_Sums_in_cod1 f1) by Th46; hence Partial_Sums(f2-f1) = Partial_Sums f2 - Partial_Sums f1 by Th46; end; theorem for f be Function of [:NAT,NAT:],ExtREAL, k be Element of NAT holds ProjMap2(Partial_Sums_in_cod1 f,k) = Partial_Sums(ProjMap2(f,k)) & ProjMap1(Partial_Sums_in_cod2 f,k) = Partial_Sums(ProjMap1(f,k)) proof let f be Function of [:NAT,NAT:],ExtREAL, k be Element of NAT; now let n be Element of NAT; ProjMap2(Partial_Sums_in_cod1 f,k).n = (Partial_Sums_in_cod1 f).(n,k) by MESFUNC9:def 7; hence ProjMap2(Partial_Sums_in_cod1 f,k).n = Partial_Sums(ProjMap2(f,k)).n by Th43; end; hence ProjMap2(Partial_Sums_in_cod1 f,k) = Partial_Sums(ProjMap2(f,k)) by FUNCT_2:def 8; now let n be Element of NAT; ProjMap1(Partial_Sums_in_cod2 f,k).n = (Partial_Sums_in_cod2 f).(k,n) by MESFUNC9:def 6; hence ProjMap1(Partial_Sums_in_cod2 f,k).n = Partial_Sums(ProjMap1(f,k)).n by Th43; end; hence ProjMap1(Partial_Sums_in_cod2 f,k) = Partial_Sums(ProjMap1(f,k)) by FUNCT_2:def 8; end; theorem Th54: for f be Function of [:NAT,NAT:],ExtREAL st f is without-infty or f is without+infty holds ProjMap1(Partial_Sums f,0) = ProjMap1(Partial_Sums_in_cod2 f,0) & ProjMap2(Partial_Sums f,0) = ProjMap2(Partial_Sums_in_cod1 f,0) proof let f be Function of [:NAT,NAT:],ExtREAL; assume A0: f is without-infty or f is without+infty; A1:now let m be Element of NAT; ProjMap1(Partial_Sums f,0).m = (Partial_Sums f).(0,m) by MESFUNC9:def 6 .= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,m) by A0,Lm8,Lm9 .= (Partial_Sums_in_cod2 f).(0,m) by DefRSM; hence ProjMap1(Partial_Sums f,0).m = ProjMap1(Partial_Sums_in_cod2 f,0).m by MESFUNC9:def 6; end; now let n be Element of NAT; ProjMap2(Partial_Sums f,0).n = (Partial_Sums f).(n,0) by MESFUNC9:def 7 .= (Partial_Sums_in_cod1 f).(n,0) by DefCSM; hence ProjMap2(Partial_Sums f,0).n = ProjMap2(Partial_Sums_in_cod1 f,0).n by MESFUNC9:def 7; end; hence thesis by A1,FUNCT_2:63; end; theorem for C,D be non empty set, F1,F2 be without-infty Function of [:C,D:],ExtREAL, c be Element of C holds ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c) proof let C,D be non empty set; let F1,F2 be without-infty Function of [:C,D:],ExtREAL; let c be Element of C; A2:dom ProjMap1(F1+F2,c) = D & dom ProjMap1(F1,c) = D & dom ProjMap1(F2,c) = D by FUNCT_2:def 1; {-infty} misses rng ProjMap1(F1,c) & {-infty} misses rng ProjMap1(F2,c) by ZFMISC_1:50,MESFUNC5:def 3; then ProjMap1(F1,c)"{-infty} = {} & ProjMap1(F2,c)"{-infty} = {} by RELAT_1:138; then dom ProjMap1(F1+F2,c) = (dom ProjMap1(F1,c) /\ dom ProjMap1(F2,c)) \ ((ProjMap1(F1,c)"{-infty} /\ ProjMap1(F2,c)"{+infty}) \/ (ProjMap1(F1,c)"{+infty} /\ ProjMap1(F2,c)"{-infty})) by A2; then A5:dom ProjMap1(F1+F2,c) = dom (ProjMap1(F1,c) + ProjMap1(F2,c)) by MESFUNC1:def 3; for d be object st d in dom ProjMap1(F1+F2,c) holds ProjMap1(F1+F2,c).d = (ProjMap1(F1,c) + ProjMap1(F2,c)).d proof let d be object; assume A3: d in dom ProjMap1(F1+F2,c); then A4: ProjMap1(F1+F2,c).d = (F1+F2).(c,d) & ProjMap1(F1,c).d = F1.(c,d) & ProjMap1(F2,c).d = F2.(c,d) by MESFUNC9:def 6; reconsider d1=d as Element of D by A3; [c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then ProjMap1(F1+F2,c).d = ProjMap1(F1,c).d + ProjMap1(F2,c).d by A4,Th7; hence thesis by A3,A5,MESFUNC1:def 3; end; hence ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c) by A5,FUNCT_1:2; end; theorem for C,D be non empty set, F1,F2 be without-infty Function of [:C,D:],ExtREAL, d be Element of D holds ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d) proof let C,D be non empty set; let F1,F2 be without-infty Function of [:C,D:],ExtREAL; let d be Element of D; A2:dom ProjMap2(F1+F2,d) = C & dom ProjMap2(F1,d) = C & dom ProjMap2(F2,d) = C by FUNCT_2:def 1; {-infty} misses rng ProjMap2(F1,d) & {-infty} misses rng ProjMap2(F2,d) by ZFMISC_1:50,MESFUNC5:def 3; then ProjMap2(F1,d)"{-infty} = {} & ProjMap2(F2,d)"{-infty} = {} by RELAT_1:138; then dom ProjMap2(F1+F2,d) = (dom ProjMap2(F1,d) /\ dom ProjMap2(F2,d)) \ ((ProjMap2(F1,d)"{-infty} /\ ProjMap2(F2,d)"{+infty}) \/ (ProjMap2(F1,d)"{+infty} /\ ProjMap2(F2,d)"{-infty})) by A2; then A5:dom ProjMap2(F1+F2,d) = dom (ProjMap2(F1,d) + ProjMap2(F2,d)) by MESFUNC1:def 3; for c be object st c in dom ProjMap2(F1+F2,d) holds ProjMap2(F1+F2,d).c = (ProjMap2(F1,d) + ProjMap2(F2,d)).c proof let c be object; assume A3: c in dom ProjMap2(F1+F2,d); then A4: ProjMap2(F1+F2,d).c = (F1+F2).(c,d) & ProjMap2(F1,d).c = F1.(c,d) & ProjMap2(F2,d).c = F2.(c,d) by MESFUNC9:def 7; reconsider c1=c as Element of C by A3; [c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then ProjMap2(F1+F2,d).c = ProjMap2(F1,d).c + ProjMap2(F2,d).c by A4,Th7; hence thesis by A3,A5,MESFUNC1:def 3; end; hence ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d) by A5,FUNCT_1:2; end; theorem for C,D be non empty set, F1,F2 be without+infty Function of [:C,D:],ExtREAL, c be Element of C holds ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c) proof let C,D be non empty set; let F1,F2 be without+infty Function of [:C,D:],ExtREAL; let c be Element of C; A2:dom ProjMap1(F1+F2,c) = D & dom ProjMap1(F1,c) = D & dom ProjMap1(F2,c) = D by FUNCT_2:def 1; {+infty} misses rng ProjMap1(F1,c) & {+infty} misses rng ProjMap1(F2,c) by ZFMISC_1:50,MESFUNC5:def 4; then ProjMap1(F1,c)"{+infty} = {} & ProjMap1(F2,c)"{+infty} = {} by RELAT_1:138; then dom ProjMap1(F1+F2,c) = (dom ProjMap1(F1,c) /\ dom ProjMap1(F2,c)) \ ((ProjMap1(F1,c)"{-infty} /\ ProjMap1(F2,c)"{+infty}) \/ (ProjMap1(F1,c)"{+infty} /\ ProjMap1(F2,c)"{-infty})) by A2; then A5:dom ProjMap1(F1+F2,c) = dom (ProjMap1(F1,c) + ProjMap1(F2,c)) by MESFUNC1:def 3; for d be object st d in dom ProjMap1(F1+F2,c) holds ProjMap1(F1+F2,c).d = (ProjMap1(F1,c) + ProjMap1(F2,c)).d proof let d be object; assume A3: d in dom ProjMap1(F1+F2,c); then A4: ProjMap1(F1+F2,c).d = (F1+F2).(c,d) & ProjMap1(F1,c).d = F1.(c,d) & ProjMap1(F2,c).d = F2.(c,d) by MESFUNC9:def 6; reconsider d1=d as Element of D by A3; [c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then ProjMap1(F1+F2,c).d = ProjMap1(F1,c).d + ProjMap1(F2,c).d by A4,Th7; hence thesis by A3,A5,MESFUNC1:def 3; end; hence ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c) by A5,FUNCT_1:2; end; theorem for C,D be non empty set, F1,F2 be without+infty Function of [:C,D:],ExtREAL, d be Element of D holds ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d) proof let C,D be non empty set; let F1,F2 be without+infty Function of [:C,D:],ExtREAL; let d be Element of D; A2:dom ProjMap2(F1+F2,d) = C & dom ProjMap2(F1,d) = C & dom ProjMap2(F2,d) = C by FUNCT_2:def 1; {+infty} misses rng ProjMap2(F1,d) & {+infty} misses rng ProjMap2(F2,d) by ZFMISC_1:50,MESFUNC5:def 4; then ProjMap2(F1,d)"{+infty} = {} & ProjMap2(F2,d)"{+infty} = {} by RELAT_1:138; then dom ProjMap2(F1+F2,d) = (dom ProjMap2(F1,d) /\ dom ProjMap2(F2,d)) \ ((ProjMap2(F1,d)"{-infty} /\ ProjMap2(F2,d)"{+infty}) \/ (ProjMap2(F1,d)"{+infty} /\ ProjMap2(F2,d)"{-infty})) by A2; then A5:dom ProjMap2(F1+F2,d) = dom (ProjMap2(F1,d) + ProjMap2(F2,d)) by MESFUNC1:def 3; for c be object st c in dom ProjMap2(F1+F2,d) holds ProjMap2(F1+F2,d).c = (ProjMap2(F1,d) + ProjMap2(F2,d)).c proof let c be object; assume A3: c in dom ProjMap2(F1+F2,d); then A4: ProjMap2(F1+F2,d).c = (F1+F2).(c,d) & ProjMap2(F1,d).c = F1.(c,d) & ProjMap2(F2,d).c = F2.(c,d) by MESFUNC9:def 7; reconsider c1=c as Element of C by A3; [c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then ProjMap2(F1+F2,d).c = ProjMap2(F1,d).c + ProjMap2(F2,d).c by A4,Th7; hence thesis by A3,A5,MESFUNC1:def 3; end; hence ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d) by A5,FUNCT_1:2; end; theorem for C,D be non empty set, F1 be without-infty Function of [:C,D:],ExtREAL, F2 be without+infty Function of [:C,D:],ExtREAL, c be Element of C holds ProjMap1(F1-F2,c) = ProjMap1(F1,c) - ProjMap1(F2,c) & ProjMap1(F2-F1,c) = ProjMap1(F2,c) - ProjMap1(F1,c) proof let C,D be non empty set; let F1 be without-infty Function of [:C,D:],ExtREAL; let F2 be without+infty Function of [:C,D:],ExtREAL; let c be Element of C; A2:dom ProjMap1(F1-F2,c) = D & dom ProjMap1(F2-F1,c) = D & dom ProjMap1(F1,c) = D & dom ProjMap1(F2,c) = D by FUNCT_2:def 1; {-infty} misses rng ProjMap1(F1,c) & {+infty} misses rng ProjMap1(F2,c) by ZFMISC_1:50,MESFUNC5:def 3,def 4; then B1:ProjMap1(F1,c)"{-infty} = {} & ProjMap1(F2,c)"{+infty} = {} by RELAT_1:138; then dom ProjMap1(F1-F2,c) = (dom ProjMap1(F1,c) /\ dom ProjMap1(F2,c)) \ ((ProjMap1(F1,c)"{-infty} /\ ProjMap1(F2,c)"{-infty}) \/ (ProjMap1(F1,c)"{+infty} /\ ProjMap1(F2,c)"{+infty})) by A2; then A5:dom ProjMap1(F1-F2,c) = dom (ProjMap1(F1,c) - ProjMap1(F2,c)) by MESFUNC1:def 4; dom ProjMap1(F2-F1,c) = (dom ProjMap1(F2,c) /\ dom ProjMap1(F1,c)) \ ((ProjMap1(F2,c)"{+infty} /\ ProjMap1(F1,c)"{+infty}) \/ (ProjMap1(F2,c)"{-infty} /\ ProjMap1(F1,c)"{-infty})) by A2,B1; then A6:dom ProjMap1(F2-F1,c) = dom (ProjMap1(F2,c) - ProjMap1(F1,c)) by MESFUNC1:def 4; for d be object st d in dom ProjMap1(F1-F2,c) holds ProjMap1(F1-F2,c).d = (ProjMap1(F1,c) - ProjMap1(F2,c)).d proof let d be object; assume A3: d in dom ProjMap1(F1-F2,c); then A4: ProjMap1(F1-F2,c).d = (F1-F2).(c,d) & ProjMap1(F1,c).d = F1.(c,d) & ProjMap1(F2,c).d = F2.(c,d) by MESFUNC9:def 6; reconsider d1=d as Element of D by A3; [c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then ProjMap1(F1-F2,c).d = ProjMap1(F1,c).d - ProjMap1(F2,c).d by A4,Th7; hence thesis by A3,A5,MESFUNC1:def 4; end; hence ProjMap1(F1-F2,c) = ProjMap1(F1,c) - ProjMap1(F2,c) by A5,FUNCT_1:2; for d be object st d in dom ProjMap1(F2-F1,c) holds ProjMap1(F2-F1,c).d = (ProjMap1(F2,c) - ProjMap1(F1,c)).d proof let d be object; assume A3: d in dom ProjMap1(F2-F1,c); then A4: ProjMap1(F2-F1,c).d = (F2-F1).(c,d) & ProjMap1(F1,c).d = F1.(c,d) & ProjMap1(F2,c).d = F2.(c,d) by MESFUNC9:def 6; reconsider d1=d as Element of D by A3; [c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then ProjMap1(F2-F1,c).d = ProjMap1(F2,c).d - ProjMap1(F1,c).d by A4,Th7; hence thesis by A3,A6,MESFUNC1:def 4; end; hence ProjMap1(F2-F1,c) = ProjMap1(F2,c) - ProjMap1(F1,c) by A6,FUNCT_1:2; end; theorem for C,D be non empty set, F1 be without-infty Function of [:C,D:],ExtREAL, F2 be without+infty Function of [:C,D:],ExtREAL, d be Element of D holds ProjMap2(F1-F2,d) = ProjMap2(F1,d) - ProjMap2(F2,d) & ProjMap2(F2-F1,d) = ProjMap2(F2,d) - ProjMap2(F1,d) proof let C,D be non empty set; let F1 be without-infty Function of [:C,D:],ExtREAL; let F2 be without+infty Function of [:C,D:],ExtREAL; let d be Element of D; A2:dom ProjMap2(F1-F2,d) = C & dom ProjMap2(F2-F1,d) = C & dom ProjMap2(F1,d) = C & dom ProjMap2(F2,d) = C by FUNCT_2:def 1; {-infty} misses rng ProjMap2(F1,d) & {+infty} misses rng ProjMap2(F2,d) by ZFMISC_1:50,MESFUNC5:def 3,def 4; then B1:ProjMap2(F1,d)"{-infty} = {} & ProjMap2(F2,d)"{+infty} = {} by RELAT_1:138; then dom ProjMap2(F1-F2,d) = (dom ProjMap2(F1,d) /\ dom ProjMap2(F2,d)) \ ((ProjMap2(F1,d)"{-infty} /\ ProjMap2(F2,d)"{-infty}) \/ (ProjMap2(F1,d)"{+infty} /\ ProjMap2(F2,d)"{+infty})) by A2; then A5:dom ProjMap2(F1-F2,d) = dom (ProjMap2(F1,d) - ProjMap2(F2,d)) by MESFUNC1:def 4; dom ProjMap2(F2-F1,d) = (dom ProjMap2(F2,d) /\ dom ProjMap2(F1,d)) \ ((ProjMap2(F2,d)"{+infty} /\ ProjMap2(F1,d)"{+infty}) \/ (ProjMap2(F2,d)"{-infty} /\ ProjMap2(F1,d)"{-infty})) by A2,B1; then A6:dom ProjMap2(F2-F1,d) = dom (ProjMap2(F2,d) - ProjMap2(F1,d)) by MESFUNC1:def 4; for c be object st c in dom ProjMap2(F1-F2,d) holds ProjMap2(F1-F2,d).c = (ProjMap2(F1,d) - ProjMap2(F2,d)).c proof let c be object; assume A3: c in dom ProjMap2(F1-F2,d); then A4: ProjMap2(F1-F2,d).c = (F1-F2).(c,d) & ProjMap2(F1,d).c = F1.(c,d) & ProjMap2(F2,d).c = F2.(c,d) by MESFUNC9:def 7; reconsider c1=c as Element of C by A3; [c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then ProjMap2(F1-F2,d).c = ProjMap2(F1,d).c - ProjMap2(F2,d).c by A4,Th7; hence thesis by A3,A5,MESFUNC1:def 4; end; hence ProjMap2(F1-F2,d) = ProjMap2(F1,d) - ProjMap2(F2,d) by A5,FUNCT_1:2; for c be object st c in dom ProjMap2(F2-F1,d) holds ProjMap2(F2-F1,d).c = (ProjMap2(F2,d) - ProjMap2(F1,d)).c proof let c be object; assume A3: c in dom ProjMap2(F2-F1,d); then A4: ProjMap2(F2-F1,d).c = (F2-F1).(c,d) & ProjMap2(F1,d).c = F1.(c,d) & ProjMap2(F2,d).c = F2.(c,d) by MESFUNC9:def 7; reconsider c1=c as Element of C by A3; [c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then ProjMap2(F2-F1,d).c = ProjMap2(F2,d).c - ProjMap2(F1,d).c by A4,Th7; hence thesis by A3,A6,MESFUNC1:def 4; end; hence ProjMap2(F2-F1,d) = ProjMap2(F2,d) - ProjMap2(F1,d) by A6,FUNCT_1:2; end; begin :: Nonnegative extended real valued double sequences theorem for seq be nonnegative ExtREAL_sequence st not Partial_Sums seq is convergent_to_+infty holds for n be Nat holds seq.n is Real proof let seq be nonnegative ExtREAL_sequence; assume A2:not Partial_Sums seq is convergent_to_+infty; given N be Nat such that A3: not seq.N is Real; not seq.N in REAL by A3; then A4:seq.N = +infty or seq.N = -infty by XXREAL_0:14; A6:Partial_Sums seq is non-decreasing by MESFUNC9:16; now let g be Real; assume 0 < g; take N; hereby let m be Nat; assume A7: N<=m; per cases; suppose N = 0; then (Partial_Sums seq).N = seq.N by MESFUNC9:def 1; then A9: g <= (Partial_Sums seq).N by A4,SUPINF_2:51,XXREAL_0:3; (Partial_Sums seq).N <= (Partial_Sums seq).m by A7,MESFUNC9:16,RINFSUP2:7; hence g <= (Partial_Sums seq).m by A9,XXREAL_0:2; end; suppose N <> 0; then consider N1 be Nat such that A11: N = N1 + 1 by NAT_1:6; A12: (Partial_Sums seq).N1 >= 0 by SUPINF_2:51; (Partial_Sums seq).N = (Partial_Sums seq).N1 + seq.N by A11,MESFUNC9:def 1 .= +infty by A4,SUPINF_2:51,XXREAL_0:4,A12,XXREAL_3:39; then (Partial_Sums seq).m = +infty by A6,A7,RINFSUP2:7,XXREAL_0:4; hence g <= (Partial_Sums seq).m by XXREAL_0:3; end; end; end; hence contradiction by A2,MESFUNC5:def 9; end; theorem Th62: for seq be nonnegative ExtREAL_sequence st seq is non-decreasing holds seq is convergent_to_+infty or seq is convergent_to_finite_number proof let seq be nonnegative ExtREAL_sequence; assume A1: seq is non-decreasing; now assume seq is convergent_to_-infty; then consider N be Nat such that A4: for n be Nat st N<=n holds seq.n <= -1 by MESFUNC5:def 10; seq.N <= -1 & seq.N >= 0 by SUPINF_2:51,A4; hence contradiction; end; hence thesis by A1,RINFSUP2:37,MESFUNC5:def 11; end; Lm10: for f be Function of [:NAT,NAT:],ExtREAL, n be Element of NAT st f is nonnegative holds ProjMap1(f,n) is nonnegative & ProjMap2(f,n) is nonnegative proof let f be Function of [:NAT,NAT:],ExtREAL, n be Element of NAT; assume A1: f is nonnegative; now let m be object; assume m in dom(ProjMap1(f,n)); then reconsider m1=m as Element of NAT; (ProjMap1(f,n)).m1 = f.(n,m1) by MESFUNC9:def 6; hence (ProjMap1(f,n)).m >= 0 by A1,SUPINF_2:51; end; hence ProjMap1(f,n) is nonnegative by SUPINF_2:52; now let m be object; assume m in dom(ProjMap2(f,n)); then reconsider m1=m as Element of NAT; (ProjMap2(f,n)).m1 = f.(m1,n) by MESFUNC9:def 7; hence (ProjMap2(f,n)).m >= 0 by A1,SUPINF_2:51; end; hence ProjMap2(f,n) is nonnegative by SUPINF_2:52; end; registration let f be nonnegative Function of [:NAT,NAT:],ExtREAL, n be Element of NAT; cluster ProjMap1(f,n) -> nonnegative; correctness by Lm10; cluster ProjMap2(f,n) -> nonnegative; correctness by Lm10; end; theorem Th63: for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT holds ProjMap1(Partial_Sums_in_cod2 f,m) is non-decreasing proof let f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT; set PS = ProjMap1(Partial_Sums_in_cod2 f,m); for n,j be Nat st j <= n holds PS.j <= PS.n proof let n,j be Nat; defpred Q[Nat] means PS.j <= PS.$1; A6: for k be Nat holds PS.k <= PS.(k+1) proof let k be Nat; reconsider k1=k as Element of NAT by ORDINAL1:def 12; PS.(k+1) = (Partial_Sums_in_cod2 f).(m,k+1) by MESFUNC9:def 6 .= (Partial_Sums_in_cod2 f).(m,k1) + f.(m,k+1) by DefCSM .= PS.k + f.(m,k+1) by MESFUNC9:def 6; hence thesis by SUPINF_2:51,XXREAL_3:39; end; A8: for k be Nat st k >= j & (for l be Nat st l >= j & l < k holds Q[l]) holds Q[k] proof let k be Nat; assume that A9: k >= j and A10: for l be Nat st l >= j & l < k holds Q[l]; now assume k > j; then A11: k >= j + 1 by NAT_1:13; per cases by A11,XXREAL_0:1; suppose k = j + 1; hence thesis by A6; end; suppose A12: k > j + 1; then reconsider l = k-1 as Element of NAT by NAT_1:20; k < k+1 by NAT_1:13; then A13: k > l by XREAL_1:19; k = l+1; then A14: PS.l <= PS.k by A6; PS.j <= PS.l by A10,A13,A12,XREAL_1:19; hence thesis by A14,XXREAL_0:2; end; end; hence thesis by A9,XXREAL_0:1; end; A15: for k be Nat st k >= j holds Q[k] from NAT_1:sch 9(A8); assume j <= n; hence thesis by A15; end; hence thesis by RINFSUP2:7; end; theorem Th64: for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n be Element of NAT holds ProjMap2(Partial_Sums_in_cod1 f,n) is non-decreasing proof let f be nonnegative without-infty Function of [:NAT,NAT:],ExtREAL, n be Element of NAT; A1:ProjMap1(Partial_Sums_in_cod2 f@,n) is non-decreasing by Th63; Partial_Sums_in_cod2 f@ = (Partial_Sums_in_cod1 f)@ by Th40; hence ProjMap2(Partial_Sums_in_cod1 f,n) is non-decreasing by A1,Th33; end; registration let f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT; cluster ProjMap1(Partial_Sums_in_cod2 f,m) -> non-decreasing; correctness by Th63; cluster ProjMap2(Partial_Sums_in_cod1 f,m) -> non-decreasing; correctness by Th64; end; theorem Th65: for f be nonnegative Function of [:NAT,NAT:],ExtREAL holds ( f is convergent_in_cod1 implies lim_in_cod1 f is nonnegative ) & ( f is convergent_in_cod2 implies lim_in_cod2 f is nonnegative ) proof let f be nonnegative Function of [:NAT,NAT:],ExtREAL; hereby assume A2:f is convergent_in_cod1; now let n be object; assume n in dom(lim_in_cod1 f); then reconsider n1=n as Element of NAT; A4: (lim_in_cod1 f).n = lim ProjMap2(f,n1) by D1DEF5; for k be Nat holds 0 <= ProjMap2(f,n1).k by SUPINF_2:51; hence (lim_in_cod1 f).n >= 0 by A2,A4,MESFUNC9:10; end; hence lim_in_cod1 f is nonnegative by SUPINF_2:52; end; assume A2:f is convergent_in_cod2; now let n be object; assume n in dom(lim_in_cod2 f); then reconsider n1=n as Element of NAT; A4: (lim_in_cod2 f).n = lim ProjMap1(f,n1) by D1DEF6; for k be Nat holds 0 <= ProjMap1(f,n1).k by SUPINF_2:51; hence (lim_in_cod2 f).n >= 0 by A2,A4,MESFUNC9:10; end; hence thesis by SUPINF_2:52; end; theorem for f be nonnegative Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod1 f is convergent_in_cod1 & Partial_Sums_in_cod2 f is convergent_in_cod2 by RINFSUP2:37; theorem for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT st not ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_+infty holds for n be Nat holds f.(n,m) is Real proof let f be nonnegative Function of [:NAT,NAT:],ExtREAL; let m be Element of NAT; assume A2:not ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_+infty; given N be Nat such that A3: not f.(N,m) is Real; not f.(N,m) in REAL by A3; then A4:f.(N,m) = +infty or f.(N,m) = -infty by XXREAL_0:14; reconsider N1=N as Element of NAT by ORDINAL1:def 12; now let g be Real; assume 0 < g; take N; hereby let k be Nat; assume A7: N<=k; per cases; suppose A8: N = 0; ProjMap2(Partial_Sums_in_cod1 f,m).N = (Partial_Sums_in_cod1 f).(N1,m) by MESFUNC9:def 7 .= f.(N,m) by A8,DefRSM; then A9: g <= ProjMap2(Partial_Sums_in_cod1 f,m).N by A4,SUPINF_2:51,XXREAL_0:3; ProjMap2(Partial_Sums_in_cod1 f,m).N <= ProjMap2(Partial_Sums_in_cod1 f,m).k by A7,RINFSUP2:7; hence g <= ProjMap2(Partial_Sums_in_cod1 f,m).k by A9,XXREAL_0:2; end; suppose N <> 0; then consider N2 be Nat such that A11: N = N2 + 1 by NAT_1:6; reconsider N3=N2 as Element of NAT by ORDINAL1:def 12; A12: (Partial_Sums_in_cod1 f).(N3,m) >= 0 by SUPINF_2:51; ProjMap2(Partial_Sums_in_cod1 f,m).N1 = (Partial_Sums_in_cod1 f).(N1,m) by MESFUNC9:def 7 .= (Partial_Sums_in_cod1 f).(N2,m) + f.(N1,m) by A11,DefRSM; then ProjMap2(Partial_Sums_in_cod1 f,m).N1 = +infty by A4,SUPINF_2:51,XXREAL_0:4,A12,XXREAL_3:39; then ProjMap2(Partial_Sums_in_cod1 f,m).k = +infty by XXREAL_0:4,A7,RINFSUP2:7; hence g <= ProjMap2(Partial_Sums_in_cod1 f,m).k by XXREAL_0:3; end; end; end; hence contradiction by A2,MESFUNC5:def 9; end; theorem for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT st not ProjMap1(Partial_Sums_in_cod2 f,m) is convergent_to_+infty holds for n be Nat holds f.(m,n) is Real proof let f be nonnegative Function of [:NAT,NAT:],ExtREAL; let m be Element of NAT; assume A2:not ProjMap1(Partial_Sums_in_cod2 f,m) is convergent_to_+infty; given N be Nat such that A3: not f.(m,N) is Real; not f.(m,N) in REAL by A3; then A4:f.(m,N) = +infty or f.(m,N) = -infty by XXREAL_0:14; reconsider N1=N as Element of NAT by ORDINAL1:def 12; now let g be Real; assume 0 < g; take N; hereby let k be Nat; assume A7: N<=k; per cases; suppose A8: N = 0; ProjMap1(Partial_Sums_in_cod2 f,m).N = (Partial_Sums_in_cod2 f).(m,N1) by MESFUNC9:def 6 .= f.(m,N) by A8,DefCSM; then A9: g <= ProjMap1(Partial_Sums_in_cod2 f,m).N by A4,SUPINF_2:51,XXREAL_0:3; ProjMap1(Partial_Sums_in_cod2 f,m).N <= ProjMap1(Partial_Sums_in_cod2 f,m).k by A7,RINFSUP2:7; hence g <= ProjMap1(Partial_Sums_in_cod2 f,m).k by A9,XXREAL_0:2; end; suppose N <> 0; then consider N2 be Nat such that A11: N = N2 + 1 by NAT_1:6; reconsider N3=N2 as Element of NAT by ORDINAL1:def 12; A12: (Partial_Sums_in_cod2 f).(m,N3) >= 0 by SUPINF_2:51; ProjMap1(Partial_Sums_in_cod2 f,m).N1 = (Partial_Sums_in_cod2 f).(m,N1) by MESFUNC9:def 6 .= (Partial_Sums_in_cod2 f).(m,N2) + f.(m,N1) by A11,DefCSM; then ProjMap1(Partial_Sums_in_cod2 f,m).N1 = +infty by A4,SUPINF_2:51,XXREAL_0:4,A12,XXREAL_3:39; then ProjMap1(Partial_Sums_in_cod2 f,m).k = +infty by XXREAL_0:4,A7,RINFSUP2:7; hence g <= ProjMap1(Partial_Sums_in_cod2 f,m).k by XXREAL_0:3; end; end; end; hence contradiction by A2,MESFUNC5:def 9; end; theorem for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat st (for i be Nat st i <= n holds f.(i,m) is Real) holds (Partial_Sums_in_cod1 f).(n,m) < +infty proof let f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat; assume A2: for i be Nat st i<=n holds f.(i,m) is Real; defpred P[Nat] means $1<=n implies (Partial_Sums_in_cod1 f).($1,m) < +infty; (Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM; then (Partial_Sums_in_cod1 f).(0,m) is Real by A2; then A4:P[0] by XXREAL_0:9,XREAL_0:def 1; A5:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A6: P[k]; now assume A7: k+1<=n; then A8: f.(k+1,m) is Real & f.(k+1,m) >= 0 by A2,SUPINF_2:51; (Partial_Sums_in_cod1 f).(k+1,m) = (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM; hence (Partial_Sums_in_cod1 f).(k+1,m) < +infty by A6,A7,A8,NAT_1:13,XXREAL_3:16,XXREAL_0:4; end; hence P[k+1]; end; for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); hence thesis; end; theorem for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat st (for i be Nat st i <= m holds f.(n,i) is Real) holds (Partial_Sums_in_cod2 f).(n,m) < +infty proof let f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat; assume A2: for i be Nat st i<=m holds f.(n,i) is Real; defpred P[Nat] means $1<=m implies (Partial_Sums_in_cod2 f).(n,$1) < +infty; (Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then (Partial_Sums_in_cod2 f).(n,0) is Real by A2; then A4:P[0] by XXREAL_0:9,XREAL_0:def 1; A5:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A6: P[k]; now assume A7: k+1<=m; then A8: f.(n,k+1) is Real & f.(n,k+1) >= 0 by A2,SUPINF_2:51; (Partial_Sums_in_cod2 f).(n,k+1) = (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM; hence (Partial_Sums_in_cod2 f).(n,k+1) < +infty by A6,A7,A8,NAT_1:13,XXREAL_3:16,XXREAL_0:4; end; hence P[k+1]; end; for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); hence thesis; end; theorem for f be without-infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f is convergent_in_cod1_to_-infty implies ex m be Element of NAT st ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_-infty proof let f be without-infty Function of [:NAT,NAT:],ExtREAL; assume A1: Partial_Sums f is convergent_in_cod1_to_-infty; A3:ProjMap2(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),0) = ProjMap2(Partial_Sums f,0) .= ProjMap2(Partial_Sums_in_cod1 f,0) by Th54; assume for m be Element of NAT holds not ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_-infty; hence contradiction by A1,A3; end; theorem Th72: for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat holds (for k be Element of NAT st k<=m holds not ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty) iff (for k be Element of NAT st k<=m holds lim ProjMap1(Partial_Sums_in_cod2 f,k) < +infty) proof let f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat; hereby assume A1: for k be Element of NAT st k<=m holds not ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty; hereby let k be Element of NAT; assume k<=m; then not ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty by A1; then ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_finite_number by Th62; then ex g be Real st lim ProjMap1(Partial_Sums_in_cod2 f,k) = g & for p be Real st 0

m or
not ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty;
defpred P[Nat] means $1 <= m implies
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).$1 <> +infty;
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).0
= (lim_in_cod2(Partial_Sums_in_cod2 f)).0 by MESFUNC9:def 1
.= lim ProjMap1(Partial_Sums_in_cod2 f,0) by D1DEF6; then
A5: P[0] by A3,Th72;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A7: P[k];
assume A8: k+1 <= m;
A10: (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).(k+1)
= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).k
+ (lim_in_cod2(Partial_Sums_in_cod2 f)).(k+1) by MESFUNC9:def 1;
now assume (lim_in_cod2(Partial_Sums_in_cod2 f)).(k+1) = +infty; then
lim ProjMap1(Partial_Sums_in_cod2 f,k+1) = +infty by D1DEF6;
hence contradiction by A3,A8,Th72;
end;
hence (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).(k+1)
<> +infty by A7,A8,NAT_1:13,A10,XXREAL_3:16;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A6);
hence contradiction by A2;
end;
hence
ex k be Element of NAT st k <= m
& ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty;
end;
given k be Element of NAT such that
B1: k <= m
& ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty;
lim ProjMap1(Partial_Sums_in_cod2 f,k) = +infty by B1,MESFUNC9:7; then
B2:(lim_in_cod2(Partial_Sums_in_cod2 f)).k = +infty by D1DEF6;
B3:Partial_Sums_in_cod2 f is convergent_in_cod2 by RINFSUP2:37; then
(lim_in_cod2(Partial_Sums_in_cod2 f)) is nonnegative by Th65; then
B5:(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).k
>= +infty by B2,Th4;
lim_in_cod2(Partial_Sums_in_cod2 f) is nonnegative by B3,Th65; then
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).k
<= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m
by B1,RINFSUP2:7,MESFUNC9:16;
hence (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m = +infty
by B5,XXREAL_0:2,4;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat holds
(Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 f))).m = +infty
iff
ex k be Element of NAT
st k <= m & ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_+infty
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat;
hereby assume
A1: (Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 f))).m = +infty;
lim_in_cod1(Partial_Sums_in_cod1 f)
= lim_in_cod2((Partial_Sums_in_cod1 f)@) by Th38
.= lim_in_cod2(Partial_Sums_in_cod2 f@) by Th40; then
consider k be Element of NAT such that
A2: k <= m & ProjMap1(Partial_Sums_in_cod2 f@,k) is convergent_to_+infty
by A1,Th74;
ProjMap1(Partial_Sums_in_cod2 f@,k)
= ProjMap2((Partial_Sums_in_cod2 f@)@,k) by Th32
.= ProjMap2(Partial_Sums_in_cod1 (f@)@,k) by Th40
.= ProjMap2(Partial_Sums_in_cod1 f,k) by DBLSEQ_2:7;
hence ex k be Element of NAT
st k <= m & ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_+infty
by A2;
end;
given k be Element of NAT such that
A3: k <= m & ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_+infty;
A4:ProjMap2(Partial_Sums_in_cod1 f,k)
= ProjMap2(Partial_Sums_in_cod1 (f@)@,k) by DBLSEQ_2:7
.= ProjMap2((Partial_Sums_in_cod2 f@)@,k) by Th40
.= ProjMap1(Partial_Sums_in_cod2 f@,k) by Th32;
lim_in_cod1(Partial_Sums_in_cod1 f)
= lim_in_cod2((Partial_Sums_in_cod1 f)@) by Th38
.= lim_in_cod2(Partial_Sums_in_cod2 f@) by Th40;
hence (Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 f))).m = +infty
by A3,A4,Th74;
end;
theorem Th76:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds
(Partial_Sums_in_cod1 f).(n,m) >= f.(n,m)
& (Partial_Sums_in_cod2 f).(n,m) >= f.(n,m)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat;
defpred P[Nat] means
$1 <= n implies (Partial_Sums_in_cod1 f).($1,m) >= f.($1,m);
A2:P[0] by DefRSM;
A5:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that P[k];
assume k+1 <= n;
(Partial_Sums_in_cod1 f).(k+1,m)
= (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM;
hence (Partial_Sums_in_cod1 f).(k+1,m) >= f.(k+1,m)
by SUPINF_2:51,XXREAL_3:39;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A5);
hence (Partial_Sums_in_cod1 f).(n,m) >= f.(n,m);
defpred Q[Nat] means
$1 <= m implies (Partial_Sums_in_cod2 f).(n,$1) >= f.(n,$1);
A2:Q[0] by DefCSM;
A5:for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat such that Q[k];
assume k+1 <= m;
(Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM;
hence (Partial_Sums_in_cod2 f).(n,k+1) >= f.(n,k+1)
by SUPINF_2:51,XXREAL_3:39;
end;
for k be Nat holds Q[k] from NAT_1:sch 2(A2,A5);
hence (Partial_Sums_in_cod2 f).(n,m) >= f.(n,m);
end;
theorem Th77:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT
st (ex k be Element of NAT st k <= m
& ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty)
holds
ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m)
is convergent_to_+infty
& lim(ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m)) = +infty
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
m be Element of NAT;
given k be Element of NAT such that
A2: k<=m & ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty;
A5: for g be Real st 0 < g
ex N be Nat st for n be Nat st N<=n holds
g <= ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m).n
proof
let g be Real;
assume 0

= n+1; then A17: k = n+1 by A16,XXREAL_0:1; then A18: (Partial_Sums(lim_in_cod1 Partial_Sums_in_cod1 f)).k = (Partial_Sums(lim_in_cod1 Partial_Sums_in_cod1 f)).n + (lim_in_cod1 Partial_Sums_in_cod1 f).(n+1) by MESFUNC9:def 1 .= lim ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f),n1) + (lim_in_cod1 Partial_Sums_in_cod1 f).(n+1) by A15 .= lim ProjMap2(Partial_Sums f,n1) + (lim_in_cod1 Partial_Sums_in_cod1 f).(n+1) by Lm8 .= lim ProjMap2(Partial_Sums f,n1) + lim ProjMap2(Partial_Sums_in_cod1 f,k) by A17,D1DEF5; consider Gn be Real such that A19: lim ProjMap2(Partial_Sums f,n1) = Gn & for p be Real st 0

= I1 & I >= I2 by XXREAL_0:25;
now let i be Nat;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
assume I<=i; then
I1<=i & I2<=i by A27,XXREAL_0:2; then
|. ProjMap2(Partial_Sums f,n1).i - Gn .| < p/2
& |. ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1 .| < p/2
by A19,A20,A25,A26; then
A28: |. ProjMap2(Partial_Sums f,n1).i - Gn .|
+ |. ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1 .| < p/2+p/2
by XXREAL_3:64;
A29: ProjMap2(Partial_Sums f,k).i1
= (Partial_Sums f).(i,k) by MESFUNC9:def 7
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,k) by Lm8
.= (Partial_Sums_in_cod1 f).(i,k)
+ (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,n)
by A17,Th47
.= (Partial_Sums f).(i,n) + (Partial_Sums_in_cod1 f).(i,k) by Lm8
.= ProjMap2(Partial_Sums f,n1).i1
+ (Partial_Sums_in_cod1 f).(i,k) by MESFUNC9:def 7
.= ProjMap2(Partial_Sums f,n1).i1
+ ProjMap2(Partial_Sums_in_cod1 f,k).i1 by MESFUNC9:def 7;
ProjMap2(Partial_Sums_in_cod1 f,k).i1 <> -infty by SUPINF_2:51; then
A30: ProjMap2(Partial_Sums_in_cod1 f,k).i1 - Gn1a <> -infty
by XXREAL_3:19; then
A31: (ProjMap2(Partial_Sums_in_cod1 f,k).i1 - Gn1a) + Gn1a <> -infty
by XXREAL_3:17;
ProjMap2(Partial_Sums f,n1).i1 >= 0 by SUPINF_2:51; then
A32: ProjMap2(Partial_Sums f,n1).i - Gna <> -infty by XXREAL_3:19;
ProjMap2(Partial_Sums f,n1).i
= ProjMap2(Partial_Sums f,n1).i - Gna + Gna
& ProjMap2(Partial_Sums_in_cod1 f,k).i
= ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a + Gn1a
by XXREAL_3:22; then
ProjMap2(Partial_Sums f,k).i
= (ProjMap2(Partial_Sums f,n1).i - Gna)
+ (((ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a) + Gn1a) + Gna)
by A29,A31,A32,XXREAL_3:29
.= (ProjMap2(Partial_Sums f,n1).i - Gna)
+ ( (ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a) + (Gn1a + Gna) )
by XXREAL_3:29
.= (ProjMap2(Partial_Sums f,n1).i - Gna)
+ (ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a) + (Gna + Gn1a)
by A30,A32,XXREAL_3:29; then
ProjMap2(Partial_Sums f,k).i - G
= (ProjMap2(Partial_Sums f,n1).i - Gna)
+ (ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a)
by XXREAL_3:22; then
|. ProjMap2(Partial_Sums f,k).i - G .|
<= |. ProjMap2(Partial_Sums f,n1).i - Gna .|
+ |. ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a .|
by EXTREAL1:24;
hence |. ProjMap2(Partial_Sums f,k).i - G .| < p by A28,XXREAL_0:2;
end;
hence thesis;
end;
hence (Partial_Sums(lim_in_cod1 Partial_Sums_in_cod1 f)).k
= lim ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f),k)
by A18,A19,A20,A21,A22,MESFUNC5:def 12;
end;
end;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A13,A14);
hence thesis;
end;
theorem
for f be without-infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums f is convergent_in_cod2_to_finite iff
Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite
proof
let f be without-infty Function of [:NAT,NAT:],ExtREAL;
hereby assume Partial_Sums f is convergent_in_cod2_to_finite; then
(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f))@
is convergent_in_cod1_to_finite by Th36; then
Partial_Sums_in_cod1(Partial_Sums_in_cod1 f)@
is convergent_in_cod1_to_finite by Th40; then
Partial_Sums_in_cod1(Partial_Sums_in_cod2 f@)
is convergent_in_cod1_to_finite by Th40; then
Partial_Sums (f@) is convergent_in_cod1_to_finite by Lm8; then
Partial_Sums_in_cod1 (f@) is convergent_in_cod1_to_finite
by Th79; then
(Partial_Sums_in_cod2 f)@ is convergent_in_cod1_to_finite by Th40;
hence Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite by Th36;
end;
assume Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite; then
(Partial_Sums_in_cod2 f)@ is convergent_in_cod1_to_finite by Th36; then
Partial_Sums_in_cod1 (f@) is convergent_in_cod1_to_finite by Th40; then
Partial_Sums (f@) is convergent_in_cod1_to_finite by Th79; then
Partial_Sums_in_cod1(Partial_Sums_in_cod2 f@)
is convergent_in_cod1_to_finite by Lm8; then
Partial_Sums_in_cod1(Partial_Sums_in_cod1 f)@
is convergent_in_cod1_to_finite by Th40; then
(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f))@
is convergent_in_cod1_to_finite by Th40;
hence Partial_Sums f is convergent_in_cod2_to_finite by Th36;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL st
Partial_Sums f is convergent_in_cod2_to_finite
holds
for m be Element of NAT holds
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m
= lim(ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m))
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
assume Partial_Sums f is convergent_in_cod2_to_finite; then
Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)
is convergent_in_cod2_to_finite by Lm8; then
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f))@
is convergent_in_cod1_to_finite by Th36; then
Partial_Sums_in_cod2(Partial_Sums_in_cod2 f)@
is convergent_in_cod1_to_finite by Th40; then
A1:Partial_Sums (f@) is convergent_in_cod1_to_finite by Th40;
hereby let m be Element of NAT;
lim_in_cod2(Partial_Sums_in_cod2 f)
= lim_in_cod1((Partial_Sums_in_cod2 f)@) by Th38
.= lim_in_cod1(Partial_Sums_in_cod1 (f@)) by Th40; then
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m
= lim(ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 (f@)),m))
by A1,Th80
.= lim(ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod1 f)@,m)) by Th40
.= lim(ProjMap2((Partial_Sums_in_cod2(Partial_Sums_in_cod1 f))@,m))
by Th40;
hence (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m
= lim(ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m)) by Th32;
end;
end;
:: Fatou's Lemma for Double Sequence
theorem Th83:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence st
(for m be Element of NAT holds seq.m = lim_inf ProjMap2(f,m))
holds Sum seq <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence;
assume
A1: for m be Element of NAT holds seq.m = lim_inf ProjMap2(f,m);
A2:for m be Element of NAT holds
for N,n be Element of NAT st n>=N holds
(inferior_realsequence ProjMap2(f,m)).N <= f.(n,m)
proof
let m be Element of NAT;
let N,n be Element of NAT;
assume n >= N; then
A4: (inferior_realsequence ProjMap2(f,m)).N
<= (inferior_realsequence ProjMap2(f,m)).n by RINFSUP2:7;
(inferior_realsequence ProjMap2(f,m)).n <= (ProjMap2(f,m)).n
by RINFSUP2:8; then
(inferior_realsequence ProjMap2(f,m)).n <= f.(n,m) by MESFUNC9:def 7;
hence (inferior_realsequence ProjMap2(f,m)).N <= f.(n,m)
by A4,XXREAL_0:2;
end;
deffunc F(Element of NAT) = inferior_realsequence ProjMap2(f,$1);
deffunc G(Element of NAT,Element of NAT)
= (inferior_realsequence ProjMap2(f,$2)).$1;
consider g be Function of [:NAT,NAT:],ExtREAL such that
A5: for n be Element of NAT for m be Element of NAT holds
g.(n,m) = G(n,m) from BINOP_1:sch 4;
now let z be object;
per cases;
suppose z in dom g; then
consider n,m be object such that
D1: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by D1;
g.(n,m) = (inferior_realsequence ProjMap2(f,m)).n by A5; then
consider Y be non empty Subset of ExtREAL such that
D2: Y = {ProjMap2(f,m).k where k is Nat : n<=k}
& g.z = inf Y by D1,RINFSUP2:def 6;
for x be ExtReal st x in Y holds 0 <= x
proof
let x be ExtReal;
assume x in Y; then
ex k be Nat st x = ProjMap2(f,m).k & n <= k by D2;
hence 0 <= x by SUPINF_2:51;
end; then
0 is LowerBound of Y by XXREAL_2:def 2;
hence 0 <= g.z by D2,XXREAL_2:def 4;
end;
suppose not z in dom g;
hence 0 <= g.z by FUNCT_1:def 2;
end;
end; then
g is nonnegative by SUPINF_2:51; then
reconsider g as nonnegative without-infty Function of [:NAT,NAT:],ExtREAL;
A6:for m be Element of NAT holds
for N,n be Element of NAT st n>=N holds
(Partial_Sums_in_cod2 g).(N,m) <= (Partial_Sums_in_cod2 f).(n,m)
proof
let m be Element of NAT;
let N,n be Element of NAT;
assume A7: n >= N;
defpred P[Nat] means
(Partial_Sums_in_cod2 g).(N,$1) <= (Partial_Sums_in_cod2 f).(n,$1);
A8: (Partial_Sums_in_cod2 g).(N,0) = g.(N,0) by DefCSM
.= (inferior_realsequence ProjMap2(f,0)).N by A5;
(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then
A9: P[0] by A2,A7,A8;
A10:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
assume A11: P[k];
g.(N,k1+1) = (inferior_realsequence ProjMap2(f,k1+1)).N by A5; then
A12: g.(N,k1+1) <= f.(n,k1+1) by A2,A7;
(Partial_Sums_in_cod2 g).(N,k+1)
= (Partial_Sums_in_cod2 g).(N,k) + g.(N,k1+1)
& (Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k1+1) by DefCSM;
hence P[k+1] by A11,A12,XXREAL_3:36;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A9,A10);
hence thesis;
end;
A13:for m be Element of NAT holds
for N,n be Element of NAT st n>=N holds
(Partial_Sums_in_cod2 g).(N,m)
<= (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f))).n
proof
let m be Element of NAT;
let N,n be Element of NAT;
assume A14: n>=N;
consider Y be non empty Subset of ExtREAL such that
A15: Y = {ProjMap2(Partial_Sums_in_cod2 f,m).k where k is Nat : n <= k}
& (inferior_realsequence(ProjMap2(Partial_Sums_in_cod2 f,m))).n = inf Y
by RINFSUP2:def 6;
for x be ExtReal st x in Y holds (Partial_Sums_in_cod2 g).(N,m) <= x
proof
let x be ExtReal;
assume x in Y; then
consider k be Nat such that
A17: x = ProjMap2(Partial_Sums_in_cod2 f,m).k & n<=k by A15;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
A18: N <= k1 by A14,A17,XXREAL_0:2;
x = (Partial_Sums_in_cod2 f).(k1,m) by A17,MESFUNC9:def 7;
hence (Partial_Sums_in_cod2 g).(N,m) <= x by A6,A18;
end; then
(Partial_Sums_in_cod2 g).(N,m) is LowerBound of Y by XXREAL_2:def 2; then
A19:(Partial_Sums_in_cod2 g).(N,m)
<= (inferior_realsequence(ProjMap2(Partial_Sums_in_cod2 f,m))).n
by A15,XXREAL_2:def 4;
consider Z be non empty Subset of ExtREAL such that
A20: Z = {(lim_in_cod2(Partial_Sums_in_cod2 f)).k where k is Nat : n <= k}
& (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f))).n = inf Z
by RINFSUP2:def 6;
for z be ExtReal st z in Z ex y be ExtReal st y in Y & y <= z
proof
let z be ExtReal;
assume z in Z; then
consider j be Nat such that
A21: z = (lim_in_cod2(Partial_Sums_in_cod2 f)).j & n <= j by A20;
reconsider j1=j as Element of NAT by ORDINAL1:def 12;
z = lim ProjMap1(Partial_Sums_in_cod2 f,j1) by A21,D1DEF6; then
A23: z = sup ProjMap1(Partial_Sums_in_cod2 f,j1) by RINFSUP2:37;
set y = ProjMap2(Partial_Sums_in_cod2 f,m).j1;
take y;
y = (Partial_Sums_in_cod2 f).(j1,m) by MESFUNC9:def 7
.= ProjMap1(Partial_Sums_in_cod2 f,j1).m by MESFUNC9:def 6;
hence y in Y & y <= z by A15,A21,A23,RINFSUP2:23;
end; then
inf Y <= inf Z by XXREAL_2:64;
hence thesis by A15,A20,A19,XXREAL_0:2;
end;
defpred Q[Nat] means
for m be Element of NAT st m = $1 holds
(Partial_Sums seq).m = lim ProjMap2(Partial_Sums_in_cod2 g,m);
now let m be Element of NAT;
assume A24: m = 0; then
(Partial_Sums seq).m = seq.0 by MESFUNC9:def 1
.= lim_inf ProjMap2(f,0) by A1
.= sup inferior_realsequence ProjMap2(f,0) by RINFSUP2:def 9; then
A26:(Partial_Sums seq).m
= lim inferior_realsequence ProjMap2(f,0) by RINFSUP2:37;
now let n be Element of NAT;
ProjMap2(Partial_Sums_in_cod2 g,0).n
= (Partial_Sums_in_cod2 g).(n,0) by MESFUNC9:def 7
.= g.(n,0) by DefCSM
.= (inferior_realsequence ProjMap2(f,0)).n by A5;
hence (inferior_realsequence ProjMap2(f,0)).n
= ProjMap2(Partial_Sums_in_cod2 g,0).n;
end;
hence (Partial_Sums seq).m = lim ProjMap2(Partial_Sums_in_cod2 g,m)
by A24,A26,FUNCT_2:63;
end; then
A28:Q[0];
P1:for m be Element of NAT holds
ProjMap2(Partial_Sums_in_cod2 g,m) is convergent
proof
let m be Element of NAT;
for j,i be Nat st i<=j holds
ProjMap2(Partial_Sums_in_cod2 g,m).i
<= ProjMap2(Partial_Sums_in_cod2 g,m).j
proof
let j,i be Nat;
reconsider i1=i, j1=j as Element of NAT by ORDINAL1:def 12;
assume B2: i <= j;
B3: ProjMap2(Partial_Sums_in_cod2 g,m).i1 = (Partial_Sums_in_cod2 g).(i,m)
& ProjMap2(Partial_Sums_in_cod2 g,m).j1 = (Partial_Sums_in_cod2 g).(j,m)
by MESFUNC9:def 7;
defpred R[Nat] means
(Partial_Sums_in_cod2 g).(i,$1) <= (Partial_Sums_in_cod2 g).(j,$1);
B4: (Partial_Sums_in_cod2 g).(i,0) = g.(i,0) by DefCSM
.= (inferior_realsequence ProjMap2(f,0)).i1 by A5;
(Partial_Sums_in_cod2 g).(j,0) = g.(j,0) by DefCSM
.= (inferior_realsequence ProjMap2(f,0)).j1 by A5; then
B5: R[0] by B2,B4,RINFSUP2:7;
B6: for l be Nat st R[l] holds R[l+1]
proof
let l be Nat;
reconsider l1=l as Element of NAT by ORDINAL1:def 12;
assume B7: R[l];
g.(i,l+1) = (inferior_realsequence ProjMap2(f,l1+1)).i1
& g.(j,l+1) = (inferior_realsequence ProjMap2(f,l1+1)).j1 by A5; then
B8: g.(i,l+1) <= g.(j,l+1) by B2,RINFSUP2:7;
(Partial_Sums_in_cod2 g).(i,l+1)
= (Partial_Sums_in_cod2 g).(i,l) + g.(i,l+1)
& (Partial_Sums_in_cod2 g).(j,l+1)
= (Partial_Sums_in_cod2 g).(j,l) + g.(j,l+1) by DefCSM;
hence R[l+1] by B7,B8,XXREAL_3:36;
end;
for l be Nat holds R[l] from NAT_1:sch 2(B5,B6);
hence thesis by B3;
end; then
ProjMap2(Partial_Sums_in_cod2 g,m) is non-decreasing by RINFSUP2:7;
hence ProjMap2(Partial_Sums_in_cod2 g,m) is convergent by RINFSUP2:37;
end;
A29:for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
assume A30: Q[k];
now let m be Element of NAT;
assume B00: m = k+1; then
B0: (Partial_Sums seq).m
= (Partial_Sums seq).k + seq.(k+1) by MESFUNC9:def 1
.= lim ProjMap2(Partial_Sums_in_cod2 g,k1) + seq.(k+1) by A30
.= lim ProjMap2(Partial_Sums_in_cod2 g,k1) + lim_inf ProjMap2(f,k+1)
by A1;
B1: lim_inf ProjMap2(f,k+1)
= sup inferior_realsequence ProjMap2(f,k1+1) by RINFSUP2:def 9
.= lim inferior_realsequence ProjMap2(f,k1+1) by RINFSUP2:37;
B9: ProjMap2(Partial_Sums_in_cod2 g,k1) is convergent by P1;
B10: inferior_realsequence ProjMap2(f,k1+1) is convergent
by RINFSUP2:37;
for n be object st n in dom(inferior_realsequence ProjMap2(f,k1+1))
holds 0. <= (inferior_realsequence ProjMap2(f,k1+1)).n
proof
let n be object;
assume n in dom(inferior_realsequence ProjMap2(f,k1+1)); then
g.(n,k1+1) = (inferior_realsequence ProjMap2(f,k1+1)).n by A5;
hence thesis by SUPINF_2:51;
end; then
C2: inferior_realsequence ProjMap2(f,k1+1) is nonnegative by SUPINF_2:52;
for i be Nat holds
ProjMap2(Partial_Sums_in_cod2 g,m).i
= ProjMap2(Partial_Sums_in_cod2 g,k1).i
+ (inferior_realsequence ProjMap2(f,k1+1)).i
proof
let i be Nat;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
ProjMap2(Partial_Sums_in_cod2 g,m).i1
= (Partial_Sums_in_cod2 g).(i,m) by MESFUNC9:def 7
.= (Partial_Sums_in_cod2 g).(i,k) + g.(i,k+1) by B00,DefCSM
.= ProjMap2(Partial_Sums_in_cod2 g,k1).i1 + g.(i,k+1) by MESFUNC9:def 7;
hence thesis by A5;
end;
hence (Partial_Sums seq).m = lim ProjMap2(Partial_Sums_in_cod2 g,m)
by B0,B1,B9,B10,C2,MESFUNC9:11;
end;
hence Q[k+1];
end;
A30: for k be Nat holds Q[k] from NAT_1:sch 2(A28,A29);
A31:
for m be Nat holds
(Partial_Sums seq).m <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f)
proof
let m be Nat;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
A32:for n be Nat holds
ProjMap2(Partial_Sums_in_cod2 g,m1).n
<= (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f))).n
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
ProjMap2(Partial_Sums_in_cod2 g,m1).n1
= (Partial_Sums_in_cod2 g).(n,m) by MESFUNC9:def 7;
hence ProjMap2(Partial_Sums_in_cod2 g,m1).n
<= (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f))).n
by A13;
end;
A33:ProjMap2(Partial_Sums_in_cod2 g,m1) is convergent by P1;
(inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f)))
is convergent by RINFSUP2:37; then
lim ProjMap2(Partial_Sums_in_cod2 g,m1)
<= lim (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f)))
by A32,A33,RINFSUP2:38; then
(Partial_Sums seq).m
<= lim (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f)))
by A30; then
(Partial_Sums seq).m
<= sup (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f)))
by RINFSUP2:37;
hence thesis by RINFSUP2:def 9;
end;
for m be object st m in dom seq holds 0<=seq.m
proof
let m be object;
assume m in dom seq; then
reconsider m1=m as Element of NAT;
E1: seq.m = lim_inf ProjMap2(f,m1) by A1
.= sup inferior_realsequence ProjMap2(f,m1) by RINFSUP2:def 9;
for n be object st n in dom(inferior_realsequence ProjMap2(f,m1))
holds 0. <= (inferior_realsequence ProjMap2(f,m1)).n
proof
let n be object;
assume n in dom(inferior_realsequence ProjMap2(f,m1)); then
g.(n,m1) = (inferior_realsequence ProjMap2(f,m1)).n by A5;
hence thesis by SUPINF_2:51;
end; then
(inferior_realsequence ProjMap2(f,m1)).0 >= 0 by SUPINF_2:51,52;
hence thesis by E1,RINFSUP2:23;
end; then
seq is nonnegative by SUPINF_2:52; then
Partial_Sums seq is non-decreasing by MESFUNC9:16; then
lim (Partial_Sums seq) <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f)
by A31,MESFUNC9:9,RINFSUP2:37;
hence thesis by MESFUNC9:def 3;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence st
(for m be Element of NAT holds seq.m = lim_inf ProjMap1(f,m))
holds Sum seq <= lim_inf lim_in_cod1(Partial_Sums_in_cod1 f)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence;
assume A1: for m be Element of NAT holds seq.m = lim_inf ProjMap1(f,m);
now let m be Element of NAT;
ProjMap1(f,m) = ProjMap2(f@,m) by Th32;
hence seq.m = lim_inf ProjMap2(f@,m) by A1;
end; then
A2:Sum seq <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f@) by Th83;
lim_in_cod2(Partial_Sums_in_cod2 f@)
= lim_in_cod1((Partial_Sums_in_cod2 f@)@) by Th38
.= lim_in_cod1(Partial_Sums_in_cod1 (f@)@) by Th40;
hence Sum seq <= lim_inf lim_in_cod1(Partial_Sums_in_cod1 f)
by A2,DBLSEQ_2:7;
end;
theorem Th85:
for f be Function of [:NAT,NAT:],ExtREAL, seq be ExtREAL_sequence, n,m be Nat
holds
( (for i,j be Nat holds f.(i,j) <= seq.i) implies
(Partial_Sums_in_cod1 f).(n,m) <= (Partial_Sums seq).n )
& ( (for i,j be Nat holds f.(i,j) <= seq.j) implies
(Partial_Sums_in_cod2 f).(n,m) <= (Partial_Sums seq).m )
proof
let f be Function of [:NAT,NAT:],ExtREAL, seq be ExtREAL_sequence,
n,m be Nat;
hereby assume
A1: for i,j be Nat holds f.(i,j) <= seq.i;
defpred P[Nat] means
(Partial_Sums_in_cod1 f).($1,m) <= (Partial_Sums seq).$1;
A2: (Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM;
(Partial_Sums seq).0 = seq.0 by MESFUNC9:def 1; then
A3: P[0] by A1,A2;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
A6: f.(k+1,m) <= seq.(k+1) by A1;
A7: (Partial_Sums_in_cod1 f).(k+1,m)
= (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM;
(Partial_Sums seq).(k+1) = (Partial_Sums seq).k + seq.(k+1)
by MESFUNC9:def 1;
hence thesis by A5,A6,A7,XXREAL_3:36;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A3,A4);
hence (Partial_Sums_in_cod1 f).(n,m) <= (Partial_Sums seq).n;
end;
assume
A1: for i,j be Nat holds f.(i,j) <= seq.j;
defpred P[Nat] means
(Partial_Sums_in_cod2 f).(n,$1) <= (Partial_Sums seq).$1;
A2:(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM;
(Partial_Sums seq).0 = seq.0 by MESFUNC9:def 1; then
A3:P[0] by A1,A2;
A4:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
A6: f.(n,k+1) <= seq.(k+1) by A1;
A7: (Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM;
(Partial_Sums seq).(k+1) = (Partial_Sums seq).k + seq.(k+1)
by MESFUNC9:def 1;
hence thesis by A5,A6,A7,XXREAL_3:36;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem Th86:
for seq be ExtREAL_sequence, r be R_eal st
(for n be Nat holds seq.n <= r) holds lim_sup seq <= r
proof
let seq be ExtREAL_sequence, r be R_eal;
assume
A1: for n be Nat holds seq.n <= r;
deffunc F(Element of NAT) = r;
consider f be Function of NAT,ExtREAL such that
A2: for n be Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
A4:for n be Nat holds f.n = r
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence f.n = r by A2;
end; then
A5:f is convergent & lim f = r by MESFUNC5:60;
for n be Nat holds seq.n <= f.n
proof
let n be Nat;
f.n = r by A4;
hence seq.n <= f.n by A1;
end; then
lim_sup seq <= lim_sup f by MESFUN10:3;
hence lim_sup seq <= r by A5,RINFSUP2:41;
end;
theorem Th87:
for seq be ExtREAL_sequence, r be R_eal st
(for n be Nat holds r <= seq.n) holds r <= lim_inf seq
proof
let seq be ExtREAL_sequence, r be R_eal;
assume
A1: for n be Nat holds r <= seq.n;
deffunc F(Element of NAT) = r;
consider f be Function of NAT,ExtREAL such that
A2: for n be Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
A4:for n be Nat holds f.n = r
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence f.n = r by A2;
end; then
A5:f is convergent & lim f = r by MESFUNC5:60;
for n be Nat holds f.n <= seq.n
proof
let n be Nat;
f.n = r by A4;
hence f.n <= seq.n by A1;
end; then
lim_inf f <= lim_inf seq by MESFUN10:3;
hence r <= lim_inf seq by A5,RINFSUP2:41;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL holds
( for i1,i2,j be Nat st i1 <= i2 holds
(Partial_Sums_in_cod1 f).(i1,j) <= (Partial_Sums_in_cod1 f).(i2,j) )
& ( for i,j1,j2 be Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 f).(i,j1) <= (Partial_Sums_in_cod2 f).(i,j2) )
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
A2:now let i1,i2,j be natural number;
assume i1 <= i2; then
consider k be Nat such that
A3: i2 = i1 + k by NAT_1:10;
defpred P[Nat] means
$1 <= k implies (Partial_Sums_in_cod1 f).(i1,j)
<= (Partial_Sums_in_cod1 f).(i1+$1,j);
A4: P[0];
A5: for l be Nat st P[l] holds P[l+1]
proof
let l be Nat;
assume A6: P[l];
now assume A7: l+1 <= k;
(Partial_Sums_in_cod1 f).(i1+l+1,j)
= (Partial_Sums_in_cod1 f).(i1+l,j) + f.(i1+l+1,j) by DefRSM; then
(Partial_Sums_in_cod1 f).(i1+l,j)
<= (Partial_Sums_in_cod1 f).(i1+l+1,j) by SUPINF_2:51,XXREAL_3:39;
hence (Partial_Sums_in_cod1 f).(i1,j)
<= (Partial_Sums_in_cod1 f).(i1+(l+1),j)
by A6,A7,NAT_1:13,XXREAL_0:2;
end;
hence P[l+1];
end;
for l be Nat holds P[l] from NAT_1:sch 2(A4,A5);
hence (Partial_Sums_in_cod1 f).(i1,j)
<= (Partial_Sums_in_cod1 f).(i2,j) by A3;
end;
now let i,j1,j2 be natural number;
assume j1 <= j2; then
consider k be Nat such that
B3: j2 = j1 + k by NAT_1:10;
defpred P[Nat] means
$1 <= k implies (Partial_Sums_in_cod2 f).(i,j1)
<= (Partial_Sums_in_cod2 f).(i,j1+$1);
B4: P[0];
B5: for l be Nat st P[l] holds P[l+1]
proof
let l be Nat;
assume B6: P[l];
now assume B7: l+1 <= k;
(Partial_Sums_in_cod2 f).(i,j1+l+1)
= (Partial_Sums_in_cod2 f).(i,j1+l) + f.(i,j1+l+1) by DefCSM; then
(Partial_Sums_in_cod2 f).(i,j1+l)
<= (Partial_Sums_in_cod2 f).(i,j1+l+1) by SUPINF_2:51,XXREAL_3:39;
hence (Partial_Sums_in_cod2 f).(i,j1)
<= (Partial_Sums_in_cod2 f).(i,j1+(l+1))
by B6,B7,NAT_1:13,XXREAL_0:2;
end;
hence P[l+1];
end;
for l be Nat holds P[l] from NAT_1:sch 2(B4,B5);
hence (Partial_Sums_in_cod2 f).(i,j1)
<= (Partial_Sums_in_cod2 f).(i,j2) by B3;
end;
hence thesis by A2;
end;
theorem Th89:
for f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat st
(for m be Element of NAT holds ProjMap2(f,m) is non-decreasing) & i<=j
holds (Partial_Sums_in_cod2 f).(i,k) <= (Partial_Sums_in_cod2 f).(j,k)
proof
let f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat;
assume that
A1: for m be Element of NAT holds ProjMap2(f,m) is non-decreasing and
A2: i <= j;
reconsider i1=i, j1=j as Element of NAT by ORDINAL1:def 12;
defpred P[Nat] means
(Partial_Sums_in_cod2 f).(i,$1) <= (Partial_Sums_in_cod2 f).(j,$1);
ProjMap2(f,0).i1 = f.(i,0) & ProjMap2(f,0).j1 = f.(j,0)
by MESFUNC9:def 7; then
ProjMap2(f,0).i1 = (Partial_Sums_in_cod2 f).(i,0) &
ProjMap2(f,0).j1 = (Partial_Sums_in_cod2 f).(j,0) by DefCSM; then
A4:P[0] by A1,A2,RINFSUP2:7;
A5:for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A6: P[n];
A7: (Partial_Sums_in_cod2 f).(i,n+1)
= (Partial_Sums_in_cod2 f).(i,n) + f.(i,n+1)
& (Partial_Sums_in_cod2 f).(j,n+1)
= (Partial_Sums_in_cod2 f).(j,n) + f.(j,n+1) by DefCSM;
A8: ProjMap2(f,n+1).i <= ProjMap2(f,n+1).j by A1,A2,RINFSUP2:7;
ProjMap2(f,n+1).i1 = f.(i,n+1) & ProjMap2(f,n+1).j1 = f.(j,n+1)
by MESFUNC9:def 7;
hence P[n+1] by A6,A7,A8,XXREAL_3:36;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat st
(for n be Element of NAT holds ProjMap1(f,n) is non-decreasing) & i<=j
holds (Partial_Sums_in_cod1 f).(k,i) <= (Partial_Sums_in_cod1 f).(k,j)
proof
let f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat;
assume that
A1: for n be Element of NAT holds ProjMap1(f,n) is non-decreasing and
A2: i <= j;
for n be Element of NAT holds ProjMap2(f@,n) is non-decreasing
proof
let n be Element of NAT;
ProjMap1(f,n) = ProjMap2(f@,n) by Th32;
hence thesis by A1;
end; then
(Partial_Sums_in_cod2 f@).(i,k) <= (Partial_Sums_in_cod2 f@).(j,k)
by A2,Th89; then
(Partial_Sums_in_cod1 f).(k,i) <= (Partial_Sums_in_cod2 f@).(j,k)
by Th39;
hence thesis by Th39;
end;
:: Moonotone Convergence Theorem for Double Sequence
theorem Th91:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence st
(for m be Element of NAT holds
ProjMap2(f,m) is non-decreasing & seq.m = lim ProjMap2(f,m))
holds
lim_in_cod2(Partial_Sums_in_cod2 f) is non-decreasing
& Sum seq = lim lim_in_cod2(Partial_Sums_in_cod2 f)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence;
assume
A1: for m be Element of NAT holds
ProjMap2(f,m) is non-decreasing & seq.m = lim ProjMap2(f,m);
now let m be Element of NAT;
ProjMap2(f,m) is non-decreasing by A1; then
ProjMap2(f,m) is convergent by RINFSUP2:37; then
lim_inf ProjMap2(f,m) = lim ProjMap2(f,m) by RINFSUP2:41;
hence seq.m = lim_inf ProjMap2(f,m) by A1;
end; then
A2:Sum seq <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f) by Th83;
A3:for n,m be Nat holds f.(n,m) <= seq.m
proof
let n,m be Nat;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
ProjMap2(f,m1) is non-decreasing by A1; then
lim ProjMap2(f,m1) = sup ProjMap2(f,m1) by RINFSUP2:37; then
A4: seq.m = sup ProjMap2(f,m1) by A1;
A5: n is Element of NAT by ORDINAL1:def 12;
dom(ProjMap2(f,m1)) = NAT by FUNCT_2:def 1; then
ProjMap2(f,m1).n <= sup rng ProjMap2(f,m1) by A5,FUNCT_1:3,XXREAL_2:4; then
ProjMap2(f,m1).n <= sup ProjMap2(f,m1) by RINFSUP2:def 1;
hence thesis by A4,A5,MESFUNC9:def 7;
end;
for n,m be Nat st m <= n holds
(lim_in_cod2(Partial_Sums_in_cod2 f)).m
<= (lim_in_cod2(Partial_Sums_in_cod2 f)).n
proof
let n,m be Nat;
assume C1: m <= n;
reconsider m1=m, n1=n as Element of NAT by ORDINAL1:def 12;
C2: (lim_in_cod2(Partial_Sums_in_cod2 f)).m
= lim ProjMap1(Partial_Sums_in_cod2 f,m1)
& (lim_in_cod2(Partial_Sums_in_cod2 f)).n
= lim ProjMap1(Partial_Sums_in_cod2 f,n1) by D1DEF6;
C3: ProjMap1(Partial_Sums_in_cod2 f,m1) is convergent
& ProjMap1(Partial_Sums_in_cod2 f,n1) is convergent by RINFSUP2:37;
for k be Nat holds ProjMap1(Partial_Sums_in_cod2 f,m1).k
<= ProjMap1(Partial_Sums_in_cod2 f,n1).k
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
ProjMap1(Partial_Sums_in_cod2 f,m1).k1 = (Partial_Sums_in_cod2 f).(m1,k1)
& ProjMap1(Partial_Sums_in_cod2 f,n1).k1 = (Partial_Sums_in_cod2 f).(n1,k1)
by MESFUNC9:def 6;
hence thesis by A1,C1,Th89;
end;
hence thesis by C2,C3,RINFSUP2:38;
end;
hence
lim_in_cod2(Partial_Sums_in_cod2 f) is non-decreasing by RINFSUP2:7; then
B1:lim_in_cod2(Partial_Sums_in_cod2 f) is convergent by RINFSUP2:37; then
B3:Sum seq <= lim lim_in_cod2(Partial_Sums_in_cod2 f) by A2,RINFSUP2:41;
for n be Nat holds
(lim_in_cod2(Partial_Sums_in_cod2 f)).n <= Sum seq
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A6: (lim_in_cod2(Partial_Sums_in_cod2 f)).n
= lim ProjMap1(Partial_Sums_in_cod2 f,n1) by D1DEF6;
A7: ProjMap1(Partial_Sums_in_cod2 f,n1) is convergent by RINFSUP2:37;
for m be Element of NAT holds 0 <= seq.m
proof
let m be Element of NAT;
for n be Nat holds 0. <= ProjMap2(f,m).n
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence 0. <= ProjMap2(f,m).n by SUPINF_2:39;
end; then
B2: 0. <= lim_inf ProjMap2(f,m) by Th87;
ProjMap2(f,m) is non-decreasing by A1; then
ProjMap2(f,m) is convergent by RINFSUP2:37; then
lim_inf ProjMap2(f,m) = lim ProjMap2(f,m) by RINFSUP2:41;
hence 0 <= seq.m by B2,A1;
end; then
seq is nonnegative by SUPINF_2:39; then
Partial_Sums seq is non-decreasing by MESFUNC9:16; then
A8: Partial_Sums seq is convergent by RINFSUP2:37;
for m be Nat holds
ProjMap1(Partial_Sums_in_cod2 f,n1).m <= (Partial_Sums seq).m
proof
let m be Nat;
m is Element of NAT by ORDINAL1:def 12; then
ProjMap1(Partial_Sums_in_cod2 f,n1).m
= (Partial_Sums_in_cod2 f).(n,m) by MESFUNC9:def 6;
hence ProjMap1(Partial_Sums_in_cod2 f,n1).m <= (Partial_Sums seq).m
by A3,Th85;
end; then
lim ProjMap1(Partial_Sums_in_cod2 f,n1) <= lim(Partial_Sums seq)
by A7,A8,RINFSUP2:38;
hence (lim_in_cod2(Partial_Sums_in_cod2 f)).n <= Sum seq
by A6,MESFUNC9:def 3;
end; then
lim_sup lim_in_cod2(Partial_Sums_in_cod2 f) <= Sum seq by Th86; then
lim lim_in_cod2(Partial_Sums_in_cod2 f) <= Sum seq by B1,RINFSUP2:41;
hence Sum seq = lim lim_in_cod2(Partial_Sums_in_cod2 f) by B3,XXREAL_0:1;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence st
(for m be Element of NAT holds
ProjMap1(f,m) is non-decreasing & seq.m = lim ProjMap1(f,m))
holds
lim_in_cod1(Partial_Sums_in_cod1 f) is non-decreasing
& Sum seq = lim lim_in_cod1(Partial_Sums_in_cod1 f)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence;
assume
A1: for m be Element of NAT holds
ProjMap1(f,m) is non-decreasing & seq.m = lim ProjMap1(f,m);
for m be Element of NAT holds
ProjMap2(f@,m) is non-decreasing & seq.m = lim ProjMap2(f@,m)
proof
let m be Element of NAT;
ProjMap1(f,m) is non-decreasing by A1;
hence ProjMap2(f@,m) is non-decreasing by Th32;
seq.m = lim ProjMap1(f,m) by A1;
hence seq.m = lim ProjMap2(f@,m) by Th32;
end; then
A2:lim_in_cod2(Partial_Sums_in_cod2 f@) is non-decreasing
& Sum seq = lim lim_in_cod2(Partial_Sums_in_cod2 f@) by Th91;
for n be Element of NAT holds
(lim_in_cod2(Partial_Sums_in_cod2 f@)).n
= (lim_in_cod1(Partial_Sums_in_cod1 f)).n
proof
let n be Element of NAT;
(lim_in_cod1(Partial_Sums_in_cod1 f)).n
= lim ProjMap2(Partial_Sums_in_cod1 f,n) by D1DEF5
.= lim ProjMap1((Partial_Sums_in_cod1 f)@,n) by Th33
.= lim ProjMap1(Partial_Sums_in_cod2 f@,n) by Th40;
hence thesis by D1DEF6;
end;
hence thesis by A2,FUNCT_2:def 8;
end;
begin :: Pringsheim sense convergence for extended real valued double sequences
theorem Th93:
for f be Function of [:NAT,NAT:],ExtREAL st
f is P-convergent_to_+infty holds
not f is P-convergent_to_-infty &
not f is P-convergent_to_finite_number
proof
let f be Function of [:NAT,NAT:],ExtREAL;
assume A1: f is P-convergent_to_+infty;
hereby assume f is P-convergent_to_-infty; then
consider N1 be Nat such that
A3: for n,m be Nat st n>=N1 & m>=N1 holds f.(n,m) <= -1;
consider N2 be Nat such that
A4: for n,m be Nat st n>=N2 & m>=N2 holds 1 <= f.(n,m) by A1;
reconsider N1,N2 as Element of NAT by ORDINAL1:def 12;
set N = max(N1,N2);
A5: N>=N1 & N>=N2 by XXREAL_0:25; then
f.(N,N) <= -1 by A3;
hence contradiction by A4,A5;
end;
assume f is P-convergent_to_finite_number; then
consider p be Real such that
A6: for e be Real st 0

=N & m>=N holds |. f.(n,m) - sup rng f .| < p proof let p be Real; assume A14: 0 < p; reconsider e=p as R_eal by XXREAL_0:def 1; sup rng f in REAL by A12,A11,XXREAL_0:14; then consider y be ExtReal such that A15: y in rng f and A16: sup rng f - e < y by A14,MEASURE6:6; consider x be object such that A17: x in dom f and A18: y=f.x by A15,FUNCT_1:def 3; consider i,j be object such that B1: i in NAT & j in NAT & x=[i,j] by A17,ZFMISC_1:def 2; reconsider i,j as Nat by B1; reconsider Ni=i, Nj=j as Element of NAT by B1; set N0=max(Ni,n0), M0=max(Nj,m0), N=max(N0,M0); take N; hereby let n,m be Nat; Ni<=N0 & n0<=N0 & Nj<=M0 & m0<=M0 & N0<=N & M0<=N by XXREAL_0:25; then B2: Ni <= N & Nj <= N by XXREAL_0:2; assume N <= n & N <= m; then Ni <=n & Nj <= m by B2,XXREAL_0:2; then f.(Ni,Nj) <= f.(n,m) by A1; then sup rng f - e < f.(n,m) by A16,A18,B1,XXREAL_0:2; then sup rng f < f.(n,m) + e by XXREAL_3:54; then sup rng f - f.(n,m) < e by XXREAL_3:55; then -e < - (sup rng f - f.(n,m)) by XXREAL_3:38; then A20: -e < f.(n,m) -sup rng f by XXREAL_3:26; A21: f.(n,m) <= sup rng f by A2; A22: now assume A23: sup rng f = sup rng f + e; e + sup rng f + -sup rng f = e + (sup rng f + -sup rng f) by A12,A11,XXREAL_3:29 .= e + 0 by XXREAL_3:7 .= e by XXREAL_3:4; hence contradiction by A14,A23,XXREAL_3:7; end; sup rng f + (0 qua ExtReal) <= sup rng f + e by A14,XXREAL_3:36; then sup rng f <= sup rng f + e by XXREAL_3:4; then sup rng f < sup rng f + e by A22,XXREAL_0:1; then f.(n,m) < sup rng f + e by A21,XXREAL_0:2; then f.(n,m) -sup rng f < e by XXREAL_3:55; hence |.f.(n,m)-sup rng f .| < p by A20,EXTREAL1:22; end; end; A24: h = sup rng f; then A25: f is P-convergent_to_finite_number by A13; hence f is P-convergent; hence thesis by A13,A24,A25,Def5; end; suppose A26: not (ex K be Real st 0 < K & for n,m be Nat holds f.(n,m) < K); now let K be Real; assume 0 < K; then consider N0,N1 be Nat such that A27: K <= f.(N0,N1) by A26; reconsider n0=N0,n1=N1 as Element of NAT by ORDINAL1:def 12; set N = max(n0,n1); B3: N >= N0 & N >= N1 by XXREAL_0:25; reconsider N as Nat; now let n,m be Nat; assume N <=n & N <= m; then N0 <= n & N1 <= m by B3,XXREAL_0:2; then f.(N0,N1) <= f.(n,m) by A1; hence K <= f.(n,m) by A27,XXREAL_0:2; end; hence ex N be Nat st for n,m be Nat st N<=n & N<=m holds K <= f.(n,m); end; then A28: f is P-convergent_to_+infty; hence A29: f is P-convergent; now assume A30: sup rng f <> +infty; f.(n0,m0) <= sup(rng f) by A2; then reconsider h=sup rng f as Element of REAL by A8,A30,XXREAL_0:14; set K=max(0,h); 0 <=K by XXREAL_0:25; then consider N0,M0 be Nat such that A31: K+1 <= f.(N0,M0) by A26; h+0 < K+1 by XREAL_1:8,XXREAL_0:25; then sup rng f < f.(N0,M0) by A31,XXREAL_0:2; hence contradiction by A2; end; hence thesis by A28,A29,Def5; end; end; end; theorem for f1,f2 be Function of [:NAT,NAT:],ExtREAL st (for n,m be Nat holds f1.(n,m) <= f2.(n,m)) holds sup rng f1 <= sup rng f2 proof let f1,f2 be Function of [:NAT,NAT:],ExtREAL; assume A1: for n,m be Nat holds f1.(n,m) <= f2.(n,m); A2:now let n,m be Element of NAT; dom f2 = [:NAT,NAT:] by FUNCT_2:def 1; then [n,m] in dom f2 by ZFMISC_1:87; then A3: f2.(n,m) in rng f2 by FUNCT_1:def 3; A4: f1.(n,m) <= f2.(n,m) by A1; sup rng f2 is UpperBound of rng f2 by XXREAL_2:def 3; then f2.(n,m) <= sup rng f2 by A3,XXREAL_2:def 1; hence f1.(n,m) <= sup rng f2 by A4,XXREAL_0:2; end; now let x be ExtReal; assume x in rng f1; then consider z be object such that A5: z in dom f1 & x=f1.z by FUNCT_1:def 3; consider n,m be object such that A6: n in NAT & m in NAT & z = [n,m] by A5,ZFMISC_1:def 2; reconsider n,m as Element of NAT by A6; x = f1.(n,m) by A5,A6; hence x <= sup rng f2 by A2; end; then sup rng f2 is UpperBound of rng f1 by XXREAL_2:def 1; hence thesis by XXREAL_2:def 3; end; theorem for f be Function of [:NAT,NAT:],ExtREAL holds for n,m be Nat holds f.(n,m) <= sup rng f proof let f be Function of [:NAT,NAT:],ExtREAL; hereby let n,m be Nat; A0: n in NAT & m in NAT by ORDINAL1:def 12; dom f = [:NAT,NAT:] by FUNCT_2:def 1; then [n,m] in dom f by A0,ZFMISC_1:87; then A1: f.(n,m) in rng f by FUNCT_1:def 3; sup rng f is UpperBound of rng f by XXREAL_2:def 3; hence f.(n,m) <= sup rng f by A1,XXREAL_2:def 1; end; end; theorem for f be Function of [:NAT,NAT:],ExtREAL, K be R_eal st (for n,m be Nat holds f.(n,m) <= K) holds sup rng f <= K proof let f be Function of [:NAT,NAT:],ExtREAL, K be R_eal; assume A1: for n,m be Nat holds f.(n,m) <= K; now let x be ExtReal; assume x in rng f; then consider z be object such that A2: z in dom f & x = f.z by FUNCT_1:def 3; consider n,m be object such that A3: n in NAT & m in NAT & z = [n,m] by A2,ZFMISC_1:def 2; reconsider n,m as Element of NAT by A3; x = f.(n,m) by A2,A3; hence x <= K by A1; end; then K is UpperBound of rng f by XXREAL_2:def 1; hence thesis by XXREAL_2:def 3; end; theorem for f be Function of [:NAT,NAT:],ExtREAL, K be R_eal st K <> +infty & (for n,m be Nat holds f.(n,m) <= K) holds sup rng f < +infty proof let f be Function of [:NAT,NAT:],ExtREAL, K be R_eal; assume A1: K <> +infty & (for n,m be Nat holds f.(n,m) <= K); now let x be ExtReal; assume x in rng f; then consider z be object such that A2: z in dom f & x = f.z by FUNCT_1:def 3; consider n,m be object such that A3: n in NAT & m in NAT & z = [n,m] by A2,ZFMISC_1:def 2; reconsider n,m as Element of NAT by A3; x = f.(n,m) by A2,A3; hence x <= K by A1; end; then K is UpperBound of rng f by XXREAL_2:def 1; then sup rng f <= K by XXREAL_2:def 3; hence thesis by A1,XXREAL_0:2,4; end; theorem Th101: for f be without-infty Function of [:NAT,NAT:],ExtREAL holds sup rng f <> +infty iff ex K be Real st 0 < K & for n,m be Nat holds f.(n,m) <= K proof let f be without-infty Function of [:NAT,NAT:],ExtREAL; A1: -infty < f.(1,1) by MESFUNC5:def 5; A2:dom f = [:NAT,NAT:] by FUNCT_2:def 1; then [1,1] in dom f by ZFMISC_1:87; then A3:f.(1,1) <= sup rng f by FUNCT_1:3,XXREAL_2:4; A4:now assume sup rng f <> +infty; then not sup rng f in {-infty,+infty} by A1,A3,TARSKI:def 2; then sup rng f in REAL by XBOOLE_0:def 3,XXREAL_0:def 4; then reconsider S = sup rng f as Real; take K = max(S,1); thus 0 < K by XXREAL_0:25; let n,m be Nat; n in NAT & m in NAT by ORDINAL1:def 12; then [n,m] in [:NAT,NAT:] by ZFMISC_1:87; then A5: f.(n,m) <= sup rng f by A2,FUNCT_1:3,XXREAL_2:4; S <= K by XXREAL_0:25; hence f.(n,m) <= K by A5,XXREAL_0:2; end; now given K be Real such that 0 < K and A6: for n,m be Nat holds f.(n,m) <= K; now let w be ExtReal; assume w in rng f; then consider z be object such that A7: z in dom f & w = f.z by FUNCT_1:def 3; consider n,m be object such that A8: n in NAT & m in NAT & z = [n,m] by A7,ZFMISC_1:def 2; reconsider n,m as Element of NAT by A8; w = f.(n,m) by A7,A8; hence w <= K by A6; end; then K is UpperBound of rng f by XXREAL_2:def 1; then sup rng f <= K by XXREAL_2:def 3; hence sup rng f <> +infty by XXREAL_0:9,XREAL_0:def 1; end; hence thesis by A4; end; theorem Th102: for f be Function of [:NAT,NAT:],ExtREAL, c be ExtReal st (for n,m be Nat holds f.(n,m) = c) holds f is P-convergent & P-lim f = c & P-lim f = sup rng f proof let f be Function of [:NAT,NAT:],ExtREAL, c be ExtReal; reconsider cc = c as R_eal by XXREAL_0:def 1; A1:dom f = [:NAT,NAT:] by FUNCT_2:def 1; c in ExtREAL by XXREAL_0:def 1; then A2:c in REAL or c in {-infty,+infty} by XBOOLE_0:def 3,XXREAL_0:def 4; assume A3:for n,m be Nat holds f.(n,m) = c; then A4:f.(1,1) = c; now let v be ExtReal; assume v in rng f; then consider z be object such that A7: z in dom f & v = f.z by FUNCT_1:def 3; consider n,m be object such that A8: n in NAT & m in NAT & z = [n,m] by A7,ZFMISC_1:def 2; reconsider n,m as Element of NAT by A8; v = f.(n,m) by A7,A8; hence v <= c by A3; end; then A5:c is UpperBound of rng f by XXREAL_2:def 1; per cases by A2,TARSKI:def 2; suppose c in REAL; then reconsider rc = c as Real; A6: now reconsider N=0 as Nat; let p be Real; assume A7: 0 < p; take N; let n1,m1 be Nat such that N <= n1 & N <= m1; f.(n1,m1) - rc = f.(n1,m1) - f.(n1,m1) by A3; hence |. f.(n1,m1) - rc .| < p by A7,EXTREAL1:16,XXREAL_3:7; end; then A8: f is P-convergent_to_finite_number; hence f is P-convergent; hence A9: P-lim f = c by A6,A8,Def5; [1,1] in dom f by A1,ZFMISC_1:87; hence thesis by A9,A5,A4,FUNCT_1:3,XXREAL_2:55; end; suppose A10: c = -infty; for p be Real st p < 0 ex N be Nat st for n,m be Nat st n >= N & m >= N holds f.(n,m) <= p proof let p be Real such that p < 0; take 0; now let n,m be Nat such that 0 <= n & 0 <= m; f.(n,m) = -infty by A3,A10; hence f.(n,m) <= p by XREAL_0:def 1,XXREAL_0:12; end; hence thesis; end; then A12:f is P-convergent_to_-infty; hence f is P-convergent; hence A13: P-lim f = c by A10,A12,Def5; [1,1] in dom f by A1,ZFMISC_1:87; hence thesis by A5,A4,A13,FUNCT_1:3,XXREAL_2:55; end; suppose A14: c = +infty; for p be Real st 0 < p ex N be Nat st for n,m be Nat st n >= N & m >= N holds p <= f.(n,m) proof let p be Real such that 0 < p; take 0; now let n,m be Nat such that n >= 0 & m >= 0; f.(n,m) = +infty by A3,A14; hence p <= f.(n,m) by XREAL_0:def 1,XXREAL_0:9; end; hence thesis; end; then A16:f is P-convergent_to_+infty; hence f is P-convergent; hence A17: P-lim f = c by A14,A16,Def5; [1,1] in dom f by A1,ZFMISC_1:87; hence thesis by A5,A4,A17,FUNCT_1:3,XXREAL_2:55; end; end; Lm8: for f be without-infty Function of [:NAT,NAT:],ExtREAL holds sup rng f in REAL or sup rng f = +infty proof let f be without-infty Function of [:NAT,NAT:],ExtREAL; A1:not -infty in rng f by MESFUNC5:def 3; dom f = [:NAT,NAT:] by FUNCT_2:def 1; then [1,1] in dom f by ZFMISC_1:87; then f.(1,1) in rng f by FUNCT_1:3; then not -infty is UpperBound of rng f by A1,XXREAL_0:6,XXREAL_2:def 1; then sup rng f <> -infty by XXREAL_2:def 3; hence thesis by XXREAL_0:14; end; theorem for f be Function of [:NAT,NAT:],ExtREAL, f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL st (for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f1.(n1,m1) <= f1.(n2,m2) ) & (for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f2.(n1,m1) <= f2.(n2,m2) ) & (for n,m be 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 proof let f be Function of [:NAT,NAT:],ExtREAL, f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL; assume that A1: for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f1.(n1,m1) <= f1.(n2,m2) and A2: for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f2.(n1,m1) <= f2.(n2,m2) and A5: for n,m be Nat holds f1.(n,m) + f2.(n,m) = f.(n,m); 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 let n1,m1,n2,m2 be Nat; assume n1<=n2 & m1<=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; end; hence A7: f is P-convergent & P-lim f = sup rng f by Th96; P1:now per cases by Lm8; suppose A9: sup rng f1 in REAL; set SE1 = sup rng f1; per cases by Lm8; suppose A10: sup rng f2 in REAL; set SE2 = sup rng f2; B1: now let p be Real; assume A11: 0 < p; then consider x1 be ExtReal such that A12: x1 in rng f1 & sup rng f1 - p/2 < x1 by A9,MEASURE6:6; consider z1 be object such that A13: z1 in dom f1 & x1 = f1.z1 by A12,FUNCT_1:def 3; consider n1,m1 be object such that A14: n1 in NAT & m1 in NAT & z1 = [n1,m1] by A13,ZFMISC_1:def 2; reconsider n1,m1 as Element of NAT by A14; consider x2 be ExtReal such that A15: x2 in rng f2 & sup rng f2 - p/2 < x2 by A10,A11,MEASURE6:6; consider z2 be object such that A16: z2 in dom f2 & x2 = f2.z2 by A15,FUNCT_1:def 3; consider n2,m2 be object such that A17: n2 in NAT & m2 in NAT & z2 = [n2,m2] by A16,ZFMISC_1:def 2; reconsider n2,m2 as Element of NAT by A17; reconsider N = max(max(n1,m1),max(n2,m2)) as Nat; take N; hereby let n,m be Nat; assume A18: n>= N & m >= N; 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 SE1 - f1.(n,m) <= SE1 - x1 & SE2 - f2.(n,m) <= SE2 - x2 by A13,A14,A16,A17,XXREAL_3:37; then A19: (SE1 - f1.(n,m)) + (SE2 - f2.(n,m)) <= (SE1 - x1) + (SE2 - x2) by XXREAL_3:36; A20: p/2 in REAL by XREAL_0:def 1; SE1 < p/2 + x1 & SE2 < p/2 + x2 by A12,A15,XXREAL_3:54; then A21: SE1 - x1 < p/2 & SE2 - x2 < p/2 by XXREAL_3:55; then A24: p/2 + (SE2 - 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) <= SE1 & f2.(n,m) <= SE2 by A6,FUNCT_1:3,XXREAL_2:4; then B2: f1.(n,m) < +infty & f2.(n,m) < +infty by A9,A10,XXREAL_0:2,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 SE2 - x2 in REAL by A10,XREAL_0:def 1; then SE1 - x1 + (SE2 - x2) < p/2 + (SE2 - x2) by A21,XXREAL_3:43; then SE1 - x1 + (SE2 - x2) < p/2 + p/2 by A24,XXREAL_0:2; then A26: (SE1 - f1.(n,m)) + (SE2 - f2.(n,m)) < p by A19,XXREAL_0:2; B5: SE1 - f1.(n,m) + (SE2 - f2.(n,m)) = SE1 - f1.(n,m) + SE2 - f2.(n,m) by A10,B2,B3,XXREAL_3:30 .= (SE2 + SE1 - f1.(n,m)) - f2.(n,m) by A9,A10,XXREAL_3:30 .= (SE1 + SE2) - (f1.(n,m) + f2.(n,m)) by A9,A10,B3,XXREAL_3:31 .= (SE1 + SE2) - f.(n,m) by A5; SE1 - f1.(n,m) >= 0 & SE2 - f2.(n,m) >= 0 by B1,XXREAL_3:40; then |. (SE1+SE2) - f.(n,m) .| < p by B5,A26,EXTREAL1:def 1; then |. -(f.(n,m) - (SE1+SE2)) .| < p by XXREAL_3:26; hence |. f.(n,m) - (SE1+SE2) .| < p by EXTREAL1:29; 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; end; suppose C1: sup rng f2 = +infty; then C2: P-lim f1 + P-lim f2 = +infty by B0,A9,XXREAL_3:def 2; now let g be Real; assume 0 < g; then consider e1 be ExtReal such that C5: e1 in rng f1 & SE1 - g/2 < e1 by A9,MEASURE6:6; consider z1 be object such that C6: z1 in dom f1 & e1 = f1.z1 by C5,FUNCT_1:def 3; consider n1,m1 be object such that C7: n1 in NAT & m1 in NAT & z1 = [n1,m1] by C6,ZFMISC_1:def 2; reconsider n1,m1 as Element of NAT by C7; g - (SE1 - g/2) in REAL & (SE1 - g/2) in REAL by A9,XREAL_0:def 1; then consider e2 be Element of ExtREAL such that C8: e2 in rng f2 & g - (SE1 - g/2) < e2 by C1,XXREAL_0:9,XXREAL_2:94; consider z2 be object such that C9: z2 in dom f2 & e2 = f2.z2 by C8,FUNCT_1:def 3; consider n2,m2 be object such that C10: n2 in NAT & m2 in NAT & z2 = [n2,m2] by C9,ZFMISC_1:def 2; reconsider n2,m2 as Element of NAT by C10; reconsider N = max(max(n2,m2),max(n1,m1)) as Nat; take N; 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 let n,m be Nat; assume n >= N & m >= N; 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: SE1 - g/2 < f1.(n,m) & g - (SE1 - g/2) < f2.(n,m) by C5,C6,C7,C8,C9,C10,XXREAL_0:2; g - (SE1 - g/2) + (SE1 - 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; end; end; then f is P-convergent_to_+infty; hence P-lim f = P-lim f1 + P-lim f2 by C2,A7,Def5; end; end; suppose D1: sup rng f1 = +infty; per cases by Lm8; suppose D3: sup rng f2 in REAL; set SE2 = sup rng f2; D2: P-lim f1 + P-lim f2 = +infty by B0,D1,D3,XXREAL_3:def 2; now let g be Real; assume 0 < g; then consider e2 be ExtReal such that D5: e2 in rng f2 & SE2 - g/2 < e2 by D3,MEASURE6:6; consider z2 be object such that D6: z2 in dom f2 & e2 = f2.z2 by D5,FUNCT_1:def 3; consider n1,m1 be object such that D7: n1 in NAT & m1 in NAT & z2 = [n1,m1] by D6,ZFMISC_1:def 2; reconsider n1,m1 as Element of NAT by D7; g - (SE2 - g/2) in REAL & SE2 - g/2 in REAL by D3,XREAL_0:def 1; then consider e1 be Element of ExtREAL such that D8: e1 in rng f1 & g - (SE2 - g/2) < e1 by D1,XXREAL_0:9,XXREAL_2:94; consider z1 be object such that D9: z1 in dom f1 & e1 = f1.z1 by D8,FUNCT_1:def 3; consider n2,m2 be object such that D10: n2 in NAT & m2 in NAT & z1 = [n2,m2] by D9,ZFMISC_1:def 2; reconsider n2,m2 as Element of NAT by D10; reconsider N = max(max(n2,m2),max(n1,m1)) as Nat; take N; 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 let n,m be Nat; assume n >= N & m >= N; 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: SE2 - g/2 < f2.(n,m) & g - (SE2 - g/2) < f1.(n,m) by D5,D6,D7,D8,D9,D10,XXREAL_0:2; g - (SE2 - g/2) + (SE2 - 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; end; end; then f is P-convergent_to_+infty; hence P-lim f = P-lim f1 + P-lim f2 by D2,A7,Def5; end; suppose E1: sup rng f2 = +infty; now let p be Real; assume E2: 0 < p; then consider n1,m1 be Nat such that E3: f1.(n1,m1) > p/2 by D1,Th101; consider n2,m2 be Nat such that E4: f2.(n2,m2) > p/2 by E1,E2,Th101; reconsider n1,n2,m1,m2 as Element of NAT by ORDINAL1:def 12; reconsider N = max(max(n2,m2),max(n1,m1)) as Nat; take N; 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 let n,m be Nat; assume n >= N & m >= N; 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; 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; end; end; end; hence P-lim f = P-lim f1 + P-lim f2; P2:P-lim f1 = sup rng f1 & P-lim f2 = sup rng f2 by A1,A2,Th96; now let n1,m1,n2,m2 be Nat; assume n1 <= n2 & m1 <= 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; end; hence thesis by P1,P2,Th96; end; theorem Th104: for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be Function of [:NAT,NAT:],ExtREAL, c be Real st 0 <= c & (for n,m be Nat holds f2.(n,m) = c * f1.(n,m)) holds sup rng f2 = c * sup rng f1 & f2 is without-infty proof let f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be Function of [:NAT,NAT:],ExtREAL, c be Real; assume that A1: 0 <= c and A3: for n,m be Nat holds f2.(n,m) = c * f1.(n,m); A6:dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] by FUNCT_2:def 1; C6:now assume -infty in rng f2; then consider z be object such that C1: z in dom f2 & -infty = f2.z by FUNCT_1:def 3; consider n,m be object such that C2: n in NAT & m in NAT & z = [n,m] by C1,ZFMISC_1:def 2; reconsider n,m as Element of NAT by C2; f2.(n,m) = -infty by C1,C2; then C3: c * f1.(n,m) = -infty by A3; then C4: f1.(n,m) = -infty or f1.(n,m) = +infty by XXREAL_3:70; z in [:NAT,NAT:] by C1; then [n,m] in dom f1 by C2,FUNCT_2:def 1; then -infty in rng f1 by A1,C3,C4,FUNCT_1:3; hence contradiction by MESFUNC5:def 3; end; then C6a:f2 is without-infty by MESFUNC5:def 3; now per cases by Lm8; suppose A4: sup rng f1 in REAL; A5: for y be UpperBound of rng f2 holds c * sup rng f1 <= y proof let y be UpperBound of rng f2; reconsider y as R_eal by XXREAL_0:def 1; per cases; suppose A8: c = 0; [1,1] in [:NAT,NAT:] by ZFMISC_1:87; then f2.(1,1) <= y by A6,FUNCT_1:3,XXREAL_2:def 1; then c * f1.(1,1) <= y by A3; hence thesis by A8; end; suppose A10: c <> 0; now let x be ExtReal; assume x in rng f1; then consider z be object such that A11: z in dom f1 & x = f1.z by FUNCT_1:def 3; consider n,m be object such that A12: n in NAT & m in NAT & z = [n,m] by A11,ZFMISC_1:def 2; reconsider n,m as Element of NAT by A12; A14: f2.(n,m) in rng f2 by A11,A12,A6,FUNCT_1:3; f2.(n,m) = c * f1.(n,m) by A3; then c * f1.(n,m) / c <= y / c by A1,A10,A14,XXREAL_2:def 1,XXREAL_3:79; hence x <= y / c by A10,A11,A12,XXREAL_3:88; end; then B14: y / c is UpperBound of rng f1 by XXREAL_2:def 1; A15: now assume A16: y = -infty; A17: [1,1] in [:NAT,NAT:] by ZFMISC_1:87; then f2.(1,1) in rng f2 by A6,FUNCT_1:3; then f2.(1,1) = -infty by A16,XXREAL_0:6,XXREAL_2:def 1; then A19: c * f1.(1,1) = -infty by A3; f1.(1,1) <= sup rng f1 by A6,A17,FUNCT_1:3,XXREAL_2:4; then A20: f1.(1,1) < +infty by A4,XXREAL_0:2,9; A21: not -infty in rng f1 by MESFUNC5:def 3; f1.(1,1) in rng f1 by A6,A17,FUNCT_1:3; hence contradiction by A19,A20,A21,XXREAL_3:70; end; per cases by A15,XXREAL_0:14; suppose y = +infty; hence thesis by XXREAL_0:4; end; suppose y in REAL; then reconsider ry = y as Real; reconsider SE1 = sup rng f1 as Real by A4; y/c = ry/c; then SE1 * c <= ry by A1,A10,B14,XXREAL_2:def 3,XREAL_1:83; hence thesis by XXREAL_3:def 5; end; end; end; now let x be ExtReal; assume x in rng f2; then consider z2 be object such that A22: z2 in dom f2 & x = f2.z2 by FUNCT_1:def 3; consider n2,m2 be object such that A23: n2 in NAT & m2 in NAT & z2 = [n2,m2] by A22,ZFMISC_1:def 2; reconsider n2,m2 as Element of NAT by A23; A24: sup rng f1 is UpperBound of rng f1 by XXREAL_2:def 3; [n2,m2] in dom f1 by A6,ZFMISC_1:87; then A25: f1.(n2,m2) <= sup rng f1 by A24,XXREAL_2:def 1,FUNCT_1:3; x = f2.(n2,m2) by A22,A23; then x = c * f1.(n2,m2) by A3; hence x <= c * sup rng f1 by A1,A25,XXREAL_3:71; end; then c * sup rng f1 is UpperBound of rng f2 by XXREAL_2:def 1; hence sup rng f2 = c * sup rng f1 by A5,XXREAL_2:def 3; end; suppose A30: sup rng f1 = +infty; per cases; suppose A27: c = 0; A28: now let n,m be Nat; f2.(n,m) = c * f1.(n,m) by A3; hence f2.(n,m) = 0 by A27; end; then P-lim f2 = sup rng f2 by Th102; hence sup rng f2 = c * sup rng f1 by A27,A28,Th102; end; suppose A29: c <> 0; A34: now let k be Real; reconsider k1 = k as Real; assume C5: 0 < k; then consider n,m be Nat such that A31: k/c < f1.(n,m) by A1,A29,A30,Th101; C10: f2.(n,m) = c * f1.(n,m) by A3; n in NAT & m in NAT by ORDINAL1:def 12; then [n,m] in dom f2 by A6,ZFMISC_1:87; then C3: f2.(n,m) <> -infty by C6,FUNCT_1:3; now per cases by C3,XXREAL_0:14; suppose C7: f2.(n,m) in REAL; f1.(n,m) > 0 & 0 >= -infty by A1,C5,A31; then C9: f1.(n,m) in REAL or f1.(n,m) = +infty by XXREAL_0:14; now assume f1.(n,m) = +infty; then c * f1.(n,m) = +infty by A1,A29,XXREAL_3:def 5; hence contradiction by A3,C7; end; then reconsider ES1 = f1.(n,m) as Real by C9; k < c * ES1 by A1,A29,A31,XREAL_1:77; hence k < f2.(n,m) by C10,XXREAL_3:def 5; end; suppose f2.(n,m) = +infty; hence k < f2.(n,m) by XREAL_0:def 1,XXREAL_0:9; end; end; hence ex n,m be Nat st not f2.(n,m) <= k; end; c * sup rng f1 = +infty by A1,A29,A30,XXREAL_3:def 5; hence sup rng f2 = c * sup rng f1 by C6a,A34,Th101; end; end; end; hence sup rng f2 = c * sup rng f1; thus f2 is without-infty by C6,MESFUNC5:def 3; end; theorem for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be Function of [:NAT,NAT:],ExtREAL, c be Real st 0 <= c & ( for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f1.(n1,m1) <= f1.(n2,m2) ) & ( for n,m be Nat holds f2.(n,m) = c * f1.(n,m) ) holds (for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f2.(n1,m1) <= f2.(n2,m2) ) & f2 is without-infty & f2 is P-convergent & P-lim f2 = sup rng f2 & P-lim f2 = c * P-lim f1 proof let f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be Function of [:NAT,NAT:],ExtREAL, c be Real; assume that A1: 0 <= c and A2: for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f1.(n1,m1) <= f1.(n2,m2) and A3: for n,m be Nat holds f2.(n,m) = c * f1.(n,m); A5:sup rng f1 = P-lim f1 by A2,Th96; thus A6: now let n1,m1,n2,m2 be Nat; assume n1 <= n2 & m1 <= m2; then c * f1.(n1,m1) <= c * f1.(n2,m2) by A1,A2,XXREAL_3:71; then f2.(n1,m1) <= c * f1.(n2,m2) by A3; hence f2.(n1,m1) <= f2.(n2,m2) by A3; end; thus f2 is without-infty by A1,A3,Th104; thus f2 is P-convergent & P-lim f2 = sup rng f2 by A6,Th96; sup rng f2 = P-lim f2 by A6,Th96; hence thesis by A1,A3,A5,Th104; end;