= -(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 -infty & seq2.m <> -infty & (seq1+seq2).m <> -infty by MESFUNC5:def 5; A13: m is Element of NAT by ORDINAL1:def 12; seq1.m - S1 qua ExtReal + (seq2.m - S2 qua ExtReal) = seq1.m - S1 qua ExtReal + seq2.m - S2 qua ExtReal by A10,XXREAL_3:30 .= -S1 qua ExtReal + (seq1.m+seq2.m) - S2 qua ExtReal by A12,XXREAL_3:29 .= (seq1+seq2).m - S1 qua ExtReal - S2 qua ExtReal by A13,Th7 .= (seq1+seq2).m - (S1 qua ExtReal + S2 qua ExtReal) by XXREAL_3:31; then |.(seq1+seq2).m - (S1+S2) qua ExtReal.| <= |.seq1.m - S1 qua ExtReal.| + |.seq2.m - S2 qua ExtReal.| by EXTREAL1:24; hence |.(seq1+seq2).m - (S1+S2) qua ExtReal.| < p by A9,XXREAL_0:2; end; hence ex n be Nat st for m be Nat st n<=m holds |.(seq1+seq2).m - (S1+S2) qua ExtReal.| < p; end; hence A14:seq1+seq2 is convergent_to_finite_number by MESFUNC5:def 8; hence seq1+seq2 is convergent; for p 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 FUNCT_4:def 8; 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 FUNCT_4:def 8; 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 FUNCT_4:def 8; 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,FUNCT_4:def 8; 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 FUNCT_4:def 8; 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,FUNCT_4:def 8; 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 FUNCT_4:def 8; 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 FUNCT_4:def 8; 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=N1 holds |.ProjMap2(Partial_Sums f,m).n - lim(ProjMap2(Partial_Sums f,m)).| < e/2 by E3; consider N2 be Nat such that B8: for n be Nat st n>=N2 holds |.ProjMap2(Partial_Sums f,k).n - lim(ProjMap2(Partial_Sums f,k)).| < e/2 by B6,E4; consider N0 be Nat such that B10: for n be Nat st n>=N0 holds |.ProjMap2(Partial_Sums_in_cod1 f,m).n - lim(ProjMap2(Partial_Sums_in_cod1 f,m)).| < e by B6,F3; reconsider N=max(max(N1,N2),N0) as Nat by TARSKI:1; take N; hereby let n be Nat; assume B9: n>=N; N >= max(N1,N2) & N >= N0 & max(N1,N2) >= N1 & max(N1,N2) >= N2 by XXREAL_0:25; then N >= N1 & N >= N2 & N >= N0 by XXREAL_0:2; then K0: n >= N1 & n >= N2 & n >= N0 by B9,XXREAL_0:2; then |.ProjMap2(Partial_Sums f,m).n - lim(ProjMap2(Partial_Sums f,m)).| < e/2 & |.ProjMap2(Partial_Sums f,k).n - lim(ProjMap2(Partial_Sums f,k)).| < e/2 & |.ProjMap2(Partial_Sums_in_cod1 f,m).n - lim(ProjMap2(Partial_Sums_in_cod1 f,m)).| < e by B7,B8,B10; then B12: |.ProjMap2(Partial_Sums f,m).n - lim(ProjMap2(Partial_Sums f,m)).| + |.ProjMap2(Partial_Sums f,k).n - lim(ProjMap2(Partial_Sums f,k)).| < e/2 + e/2 by XXREAL_3:64; K2: now assume ProjMap2(Partial_Sums f,m).n = +infty; then ProjMap2(Partial_Sums f,m).n - lim(ProjMap2(Partial_Sums f,m)) = +infty by E3,XXREAL_3:13; hence contradiction by K0,B7,XXREAL_0:3,EXTREAL1:30; end; KK2: now assume ProjMap2(Partial_Sums f,m).n = -infty; then ProjMap2(Partial_Sums f,m).n - lim(ProjMap2(Partial_Sums f,m)) = -infty by E3,XXREAL_3:14; hence contradiction by K0,B7,XXREAL_0:3,EXTREAL1:30; end; K5: now assume ProjMap2(Partial_Sums f,k).n = +infty; then ProjMap2(Partial_Sums f,k).n - lim(ProjMap2(Partial_Sums f,k)) = +infty by E4,XXREAL_3:13; hence contradiction by K0,B8,XXREAL_0:3,EXTREAL1:30; end; KK5: now assume ProjMap2(Partial_Sums f,k).n = -infty; then ProjMap2(Partial_Sums f,k).n - lim(ProjMap2(Partial_Sums f,k)) = -infty by E4,XXREAL_3:14; hence contradiction by K0,B8,XXREAL_0:3,EXTREAL1:30; end; reconsider n1=n as Element of NAT by ORDINAL1:def 12; XX2: ProjMap2(Partial_Sums f,k).n = (Partial_Sums f).(n1,k) by MESFUNC9:def 7 .= (Partial_Sums f).(n1,m) + (Partial_Sums_in_cod1 f).(n1,k) by B2,DefCSM .= ProjMap2(Partial_Sums f,m).n + (Partial_Sums_in_cod1 f).(n1,k) by MESFUNC9:def 7 .= ProjMap2(Partial_Sums f,m).n + ProjMap2(Partial_Sums_in_cod1 f,k).n by MESFUNC9:def 7; ProjMap2(Partial_Sums f,k).n in REAL by K5,KK5,XXREAL_0:14; then reconsider r4=ProjMap2(Partial_Sums f,k).n as Real; ProjMap2(Partial_Sums f,m).n in REAL by K2,KK2,XXREAL_0:14; then reconsider r5=ProjMap2(Partial_Sums f,m).n as Real; r4 = r5 + ProjMap2(Partial_Sums_in_cod1 f,k).n by XX2; then ProjMap2(Partial_Sums_in_cod1 f,k).n <> +infty & ProjMap2(Partial_Sums_in_cod1 f,k).n <> -infty; then ProjMap2(Partial_Sums_in_cod1 f,k).n in REAL by XXREAL_0:14; then reconsider r1=ProjMap2(Partial_Sums_in_cod1 f,k).n as Real; T1: ProjMap2(Partial_Sums_in_cod1 f,k).n - ( lim(ProjMap2(Partial_Sums f,k)) - lim(ProjMap2(Partial_Sums f,m)) ) = ProjMap2(Partial_Sums_in_cod1 f,k).n - (G2 - G1) by E5 .= r1 + - (G2 - G1) by XXREAL_3:def 2; T2: r5 + r1 = ProjMap2(Partial_Sums f,m).n + ProjMap2(Partial_Sums_in_cod1 f,k).n by XXREAL_3:def 2; E8: ProjMap2(Partial_Sums f,k).n + - lim(ProjMap2(Partial_Sums f,k)) = r4 + -G2 & ProjMap2(Partial_Sums f,m).n + - lim(ProjMap2(Partial_Sums f,m)) = r5 + -G1 by E7,XXREAL_3:def 2; then -( ProjMap2(Partial_Sums f,m).n - lim(ProjMap2(Partial_Sums f,m)) )= -(r5 -G1) by XXREAL_3:def 3; then ( ProjMap2(Partial_Sums f,k).n - lim(ProjMap2(Partial_Sums f,k)) ) + -( ProjMap2(Partial_Sums f,m).n - lim(ProjMap2(Partial_Sums f,m)) ) = (r4 - G2) + - (r5 - G1) by E8,XXREAL_3:def 2; then T3: ( ProjMap2(Partial_Sums f,k).n - lim(ProjMap2(Partial_Sums f,k)) ) -( ProjMap2(Partial_Sums f,m).n - lim(ProjMap2(Partial_Sums f,m)) ) = (r4 - G2) - (r5 - G1); |.ProjMap2(Partial_Sums_in_cod1 f,k).n - ( lim(ProjMap2(Partial_Sums f,k)) - lim(ProjMap2(Partial_Sums f,m)) ).| <= |.ProjMap2(Partial_Sums f,k).n - lim(ProjMap2(Partial_Sums f,k)).| + |.ProjMap2(Partial_Sums f,m).n - lim(ProjMap2(Partial_Sums f,m)).| by T1,T2,XX2,T3,EXTREAL1:32; hence |.ProjMap2(Partial_Sums_in_cod1 f,k).n - ( G2-G1 ).| < e by B12,E5,XXREAL_0:2; end; end; hence ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_finite_number by MESFUNC5:def 8; end; end; for m1 be Nat holds P[m1] from NAT_1:sch 2(A3,A4); hence ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_finite_number; end; hence Partial_Sums_in_cod1 f is convergent_in_cod1_to_finite; end; assume C0: Partial_Sums_in_cod1 f is convergent_in_cod1_to_finite; now let m be Element of NAT; defpred P[Nat] means for k be Element of NAT st k = \$1 holds ProjMap2(Partial_Sums f,k) is convergent_to_finite_number; ProjMap2(Partial_Sums f,0) = ProjMap2(Partial_Sums_in_cod1 f,0) by Th54; then C1: P[0] by C0; C2: for m be Nat st P[m] holds P[m+1] proof let m be Nat; assume C3: P[m]; reconsider m1=m as Element of NAT by ORDINAL1:def 12; hereby let k be Element of NAT; assume C4: k=m+1; then reconsider k1=k-1 as Element of NAT by NAT_1:11,21; reconsider f1 = ProjMap2(Partial_Sums f,m1), f2 = ProjMap2(Partial_Sums_in_cod1 f,m1+1) as without-infty ExtREAL_sequence; for n be Element of NAT holds ProjMap2(Partial_Sums f,k).n = (ProjMap2(Partial_Sums f,m1) + ProjMap2(Partial_Sums_in_cod1 f,m1+1)).n proof let n be Element of NAT; ProjMap2(Partial_Sums f,k).n = (Partial_Sums f).(n,m1+1) by C4,MESFUNC9:def 7 .= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m1+1) by Lm8 .= (Partial_Sums_in_cod1 f).(n,m1+1) + (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m1) by Th47 .= (Partial_Sums_in_cod1 f).(n,m1+1) + (Partial_Sums f).(n,m1) by Lm8 .= ProjMap2(Partial_Sums_in_cod1 f,m1+1).n + (Partial_Sums f).(n,m1) by MESFUNC9:def 7 .= ProjMap2(Partial_Sums_in_cod1 f,m1+1).n + ProjMap2(Partial_Sums f,m1).n by MESFUNC9:def 7; hence thesis by Th7; end; then C5: ProjMap2(Partial_Sums f,k) = f1+f2 by FUNCT_2:def 8; ProjMap2(Partial_Sums f,m1) is convergent_to_finite_number & ProjMap2(Partial_Sums_in_cod1 f,m1+1) is convergent_to_finite_number by C3,C0; hence ProjMap2(Partial_Sums f,k) is convergent_to_finite_number by C5,Th23; end; end; for m be Nat holds P[m] from NAT_1:sch 2(C1,C2); hence ProjMap2(Partial_Sums f,m) is convergent_to_finite_number; end; hence thesis; end; theorem Th80: for f be nonnegative Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod1_to_finite holds for m be Element of NAT holds (Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 f))).m = lim(ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f),m)) proof let f be nonnegative Function of [:NAT,NAT:],ExtREAL; assume A1: Partial_Sums f is convergent_in_cod1_to_finite; then A2:Partial_Sums_in_cod1 f is convergent_in_cod1_to_finite by Th79; let m be Element of NAT; defpred P[Nat] means for k be Element of NAT st k<=\$1 holds (Partial_Sums(lim_in_cod1 Partial_Sums_in_cod1 f)).k = lim(ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f),k)); now let k be Element of NAT; assume k <= 0; then A5: k = 0; A6: (Partial_Sums(lim_in_cod1 Partial_Sums_in_cod1 f)).0 = (lim_in_cod1 Partial_Sums_in_cod1 f).0 by MESFUNC9:def 1 .= lim ProjMap2(Partial_Sums_in_cod1 f,0) by D1DEF5; consider G be Real such that A7: lim ProjMap2(Partial_Sums_in_cod1 f,0) = G & for p be Real st 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) - p qua ExtReal .| < e; reconsider p1=p as ExtReal; per cases; suppose A9: p > 0; then consider N1 be Nat such that A7: for n,m be Nat st n>=N1 & m>=N1 holds |.f.(n,m)- p1.| < p by A6; A8: now let n,m be Nat; assume n>=N1 & m>=N1; then |.f.(n,m)- p qua ExtReal.| < p by A7; then f.(n,m) - p1 < p by EXTREAL1:21; then f.(n,m) < (p1+p1) by XXREAL_3:54; then f.(n,m) < 2*p1 by XXREAL_3:94; hence f.(n,m) < (2*p) by XXREAL_3:def 5; end; consider N2 be Nat such that A10: for n,m be Nat st n>=N2 & m>=N2 holds (2*p) <= f.(n,m) by A1,A9; reconsider N1,N2 as Element of NAT by ORDINAL1:def 12; set N = max(N1,N2); A11:N>=N1 & N>=N2 by XXREAL_0:25; then f.(N,N) < (2*p) by A8; hence contradiction by A11,A10; end; suppose A12: p = 0; consider N1 be Nat such that A13: for n,m be Nat st n>=N1 & m>=N1 holds |. f.(n,m)- p .| < 1 by A6; consider N2 be Nat such that A14: 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; reconsider jj =1 as ExtReal; set N = max(N1,N2); A15:N>=N1 & N>=N2 by XXREAL_0:25; then |. f.(N,N)- p1 .| < jj by A13; then f.(N,N) - p1 < jj by EXTREAL1:21; then f.(N,N) < jj + p1 by XXREAL_3:54; then f.(N,N) < 1 + 0 by A12,XXREAL_3:def 2; hence contradiction by A14,A15; end; suppose p < 0; then consider N1 be Nat such that A17: for n,m be Nat st n>=N1 & m>=N1 holds |.f.(n,m) - p .| < -p by A6; A18:now let n,m be Nat; assume n>=N1 & m>=N1; then |.f.(n,m) -p.| < -p by A17; then f.(n,m) - p1 < -p by EXTREAL1:21; then f.(n,m) < p1+(-p) by XXREAL_3:54; then f.(n,m) < p+(-p) by XXREAL_3:def 2; hence f.(n,m) < 0; end; consider N2 be Nat such that A19: 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); A20:N>=N1 & N>=N2 by XXREAL_0:25; then f.(N,N) < 0 by A18; hence contradiction by A19,A20; end; end; theorem Th94: 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) - p qua ExtReal .| < e; reconsider p1=p as ExtReal; per cases; suppose A9: p > 0; then consider N1 be Nat such that A7: for n,m be Nat st n>=N1 & m>=N1 holds |.f.(n,m)- p1.| < p by A6; A8: now let n,m be Nat; assume n>=N1 & m>=N1; then |.f.(n,m)- p qua ExtReal.| < p by A7; then -p1 < f.(n,m) - p by EXTREAL1:21; then -p1 + p < f.(n,m) by XXREAL_3:53; hence 0 < f.(n,m) by XXREAL_3:7; end; consider N2 be Nat such that A10: for n,m be Nat st n>=N2 & m>=N2 holds -(2*p) >= f.(n,m) by A1,A9; reconsider N1,N2 as Element of NAT by ORDINAL1:def 12; set N = max(N1,N2); A11:N>=N1 & N>=N2 by XXREAL_0:25; then 0 < f.(N,N) by A8; hence contradiction by A9,A11,A10; end; suppose A12: p = 0; consider N1 be Nat such that A13: for n,m be Nat st n>=N1 & m>=N1 holds |. f.(n,m)- p .| < 1 by A6; consider N2 be Nat such that A14: 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; reconsider jj =1 as ExtReal; set N = max(N1,N2); A15:N>=N1 & N>=N2 by XXREAL_0:25; then |. f.(N,N)- p1 .| < jj by A13; then -jj < f.(N,N) - p1 by EXTREAL1:21; then -jj + p < f.(N,N) by XXREAL_3:53; then -jj < f.(N,N) by A12,XXREAL_3:4; then -1 < f.(N,N) by XXREAL_3:def 3; hence contradiction by A14,A15; end; suppose A16:p < 0; then consider N1 be Nat such that A17: for n,m be Nat st n>=N1 & m>=N1 holds |.f.(n,m) - p .| < -p by A6; A18:now let n,m be Nat; assume n>=N1 & m>=N1; then |.f.(n,m) - p qua ExtReal .| < -p by A17; then -(-p1) < f.(n,m) - p1 by EXTREAL1:21; then p1 + p1 < f.(n,m) by XXREAL_3:53; then 2*p1 < f.(n,m) by XXREAL_3:94; hence (2*p) < f.(n,m) by XXREAL_3:def 5; end; consider N2 be Nat such that A19: for n,m be Nat st n>=N2 & m>=N2 holds f.(n,m) <= 2*p by A1,A16; reconsider N1,N2 as Element of NAT by ORDINAL1:def 12; set N = max(N1,N2); A20:N>=N1 & N>=N2 by XXREAL_0:25; then (2*p) < f.(N,N) by A18; hence contradiction by A19,A20; end; end; definition let f be Function of [:NAT,NAT:],ExtREAL; attr f is P-convergent means f is P-convergent_to_finite_number or f is P-convergent_to_+infty or f is P-convergent_to_-infty; end; definition let f be Function of [:NAT,NAT:],ExtREAL; assume A1:f is P-convergent; func P-lim f -> ExtReal means :Def5: (ex p be Real st it = p & (for e be Real st 0=N & m>=N holds |.f.(n,m) - it.| < e) & f is P-convergent_to_finite_number) or (it = +infty & f is P-convergent_to_+infty) or (it = -infty & f is P-convergent_to_-infty); existence proof per cases by A1; suppose A2: f is P-convergent_to_finite_number; then consider p be Real such that A3: for e be Real st 0=N & m>=N holds |.f.(n,m)- p.| < e; reconsider p as R_eal by XXREAL_0:def 1; take p; thus thesis by A2,A3; end; suppose f is P-convergent_to_+infty or f is P-convergent_to_-infty; hence thesis; end; end; uniqueness proof defpred P[ExtReal] means ( ex g be Real st \$1= g & (for p be Real st 0 < p ex N be Nat st for n,m be Nat st n>=N&m>=N holds |.f.(n,m)-\$1.| < p) & f is P-convergent_to_finite_number ) or ( \$1=+infty & f is P-convergent_to_+infty ) or ( \$1=-infty & f is P-convergent_to_-infty ); given g1,g2 be ExtReal such that A4: P[g1] and A5: P[g2] and A6: g1<>g2; per cases by A1; suppose A7: f is P-convergent_to_finite_number; then consider g be Real such that A8: g1 = g and A9: for p be Real st 0 < p ex N be Nat st for n,m be Nat st n>=N & m>=N holds |.f.(n,m)-g1.| < p and f is P-convergent_to_finite_number by A4,Th93,Th94; consider h be Real such that A10: g2 = h and A11: for p be Real st 0 < p ex N be Nat st for n,m be Nat st n>=N & m>=N holds |.f.(n,m)-g2.| < p and f is P-convergent_to_finite_number by A5,A7,Th93,Th94; reconsider g,h as Complex; A12: g - h <> 0 by A6,A8,A10; then consider N1 be Nat such that A13: for n,m be Nat st n>=N1 & m>=N1 holds |.f.(n,m)-g1.| < |.g-h.|/2 by A9; consider N2 be Nat such that A14: for n,m be Nat st n>=N2 & m>=N2 holds |.f.(n,m)-g2.| < |.g-h.|/2 by A11,A12; reconsider N1,N2 as Element of NAT by ORDINAL1:def 12; set N = max(N1,N2); B1: N>=N1 & N>=N2 by XXREAL_0:25; then A15: |.f.(N,N)-g1.| < |.g-h.|/2 by A13; A16: |.f.(N,N)-g2.| < |.g-h.|/2 by A14,B1; reconsider g,h as Complex; A17: f.(N,N)-g2 < |.g-h.|/2 by A16,EXTREAL1:21; A18: -(|.g-h.|/2 qua ExtReal) < f.(N,N)-g2 by A16,EXTREAL1:21; then reconsider w= f.(N,N) - g2 as Element of REAL by A17,XXREAL_0:48; A19: f.(N,N)-g2 in REAL by A18,A17,XXREAL_0:48; then A20: f.(N,N) <> +infty by A10; A21: -f.(N,N) + g1 = -(f.(N,N) - g1) by XXREAL_3:26; then A22: |.-f.(N,N)+g1.| < |.g-h.|/2 by A15,EXTREAL1:29; then A23: -f.(N,N)+g1 < |.g-h.|/2 by EXTREAL1:21; -(|.g-h.|/2 qua ExtReal) < -f.(N,N)+g1 by A22,EXTREAL1:21; then A24: -f.(N,N) + g1 in REAL by A23,XXREAL_0:48; A25: f.(N,N) <> -infty by A10,A19; |.g1-g2.| = |.g1 + 0. - g2.| by XXREAL_3:4 .= |.g1 + (f.(N,N) + -f.(N,N)) - g2.| by XXREAL_3:7 .= |.-f.(N,N) + g1 + f.(N,N) - g2.| by A8,A20,A25,XXREAL_3:29 .= |.-f.(N,N) + g1 +(f.(N,N) - g2).| by A10,A24,XXREAL_3:30; then |.g1-g2.| <= |.-f.(N,N) + g1.| + |.f.(N,N) - g2.| by EXTREAL1:24; then A26: |.g1-g2.| <= |.f.(N,N)-g1.| + |.f.(N,N)-g2.| by A21,EXTREAL1:29; |.f.(N,N)-g2.| < +infty & |.f.(N,N)-g2.| >= 0 by A19,EXTREAL1:41,14; then |.f.(N,N)-g2.| in REAL by XXREAL_0:14; then A27: |.f.(N,N)-g1.| + |.f.(N,N)-g2.| < (|.g-h.|/2 qua ExtReal) + |.f.(N,N)-g2.| by A15,XXREAL_3:43; |.g-h.|/2 in REAL by XREAL_0:def 1; then (|.g-h.|/2 qua ExtReal) + |.f.(N,N)-g2.| < (|.g-h.|/2 qua ExtReal) + |.g-h.|/2 by A16,XXREAL_3:43; then A28: |.f.(N,N)-g1.| + |.f.(N,N)-g2.| < (|.g-h.|/2 qua ExtReal) + |.g-h.| /2 by A27,XXREAL_0:2; g-h = g1-g2 by A8,A10,SUPINF_2:3; hence contradiction by A28,A26,EXTREAL1:12; end; suppose f is P-convergent_to_+infty or f is P-convergent_to_-infty; hence contradiction by A4,A5,A6,Th93,Th94; end; end; end; theorem for f be Function of [:NAT,NAT:],ExtREAL, r be Real st (for n,m be Nat holds f.(n,m) = r) holds f is P-convergent_to_finite_number & P-lim f = r proof let f be Function of [:NAT,NAT:],ExtREAL, r be Real; assume A1: for n,m be Nat holds f.(n,m) = r; A2:now reconsider N=1 as Nat; let p be Real; assume A3: 0 < p; take N; let n,m be Nat such that n>=N & m>=N; f.(n,m) = r by A1; hence |. f.(n,m) - r .| < p by A3,XXREAL_3:7,EXTREAL1:16; end; hence A4: f is P-convergent_to_finite_number; then f is P-convergent; hence thesis by A2,A4,Def5; end; theorem Th96: for f be Function of [:NAT,NAT:],ExtREAL st (for n1,m1,n2,m2 be Nat st n1<=n2 & m1<=m2 holds f.(n1,m1)<=f.(n2,m2)) holds f is P-convergent & P-lim f = sup rng f proof let f be Function of [:NAT,NAT:],ExtREAL; assume A1: for n1,m1,n2,m2 be Nat st n1<=n2 & m1<=m2 holds f.(n1,m1)<=f.(n2,m2); A2:now let n,m be Nat; reconsider n1=n, m1=m as Element of NAT by ORDINAL1:def 12; [n1,m1] in [:NAT,NAT:] & dom f = [:NAT,NAT:] by ZFMISC_1:def 2,FUNCT_2:def 1; then A3: f.(n1,m1) 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 A3,XXREAL_2:def 1; end; per cases; suppose A4: not ex n0,m0 be Nat st -infty < f.(n0,m0); now let x be ExtReal; assume x in rng f; then consider z be object such that B1: z in dom f & x=f.z by FUNCT_1:def 3; consider n,m be object such that B2: n in NAT & m in NAT & z=[n,m] by B1,ZFMISC_1:def 2; reconsider n,m as Nat by B2; not (-infty < f.(n,m)) by A4; hence x <= -infty by B1,B2; end; then A5: -infty is UpperBound of rng f by XXREAL_2:def 1; for y be UpperBound of rng f holds -infty <= y by XXREAL_0:5; then A6: -infty =sup rng f by A5,XXREAL_2:def 3; now reconsider N0=0 as Nat; let K be Real such that K < 0; take N0; let n,m be Nat such that N0 <= n & N0<=m; f.(n,m)=-infty by A4,XXREAL_0:6; hence f.(n,m) <= K by XXREAL_0:5; end; then A7: f is P-convergent_to_-infty; then f is P-convergent; hence thesis by A7,A6,Def5; end; suppose ex n0,m0 be Nat st -infty < f.(n0,m0); then consider n0,m0 be Nat such that A8: -infty < f.(n0,m0); reconsider n0,m0 as Element of NAT by ORDINAL1:def 12; per cases; suppose ex K be Real st for n,m be Nat holds f.(n,m) < K; then consider K be Real such that A9: 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 C1: z in dom f & x=f.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 Nat by C2; f.(n,m) < K by A9; hence x <= K by C1,C2; end; then K is UpperBound of rng f by XXREAL_2:def 1; then sup rng f <= K by XXREAL_2:def 3; then A11: sup rng f <>+infty by XXREAL_0:9,XREAL_0:def 1; A12: sup rng f <> -infty by A2,A8; then reconsider h=sup rng f as Element of REAL by A11,XXREAL_0:14; A13: for p 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;