let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: for seq being ExtREAL_sequence st ( for m being 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)) )
let seq be ExtREAL_sequence; :: thesis: ( ( for m being Element of NAT holds
( ProjMap1 (f,m) is non-decreasing & seq . m = lim (ProjMap1 (f,m)) ) ) implies ( lim_in_cod1 (Partial_Sums_in_cod1 f) is non-decreasing & Sum seq = lim (lim_in_cod1 (Partial_Sums_in_cod1 f)) ) )
assume A1: for m being Element of NAT holds
( ProjMap1 (f,m) is non-decreasing & seq . m = lim (ProjMap1 (f,m)) ) ; :: thesis: ( lim_in_cod1 (Partial_Sums_in_cod1 f) is non-decreasing & Sum seq = lim (lim_in_cod1 (Partial_Sums_in_cod1 f)) )
for m being Element of NAT holds
( ProjMap2 ((~ f),m) is non-decreasing & seq . m = lim (ProjMap2 ((~ f),m)) )
proof
let m be Element of NAT ; :: thesis: ( ProjMap2 ((~ f),m) is non-decreasing & seq . m = lim (ProjMap2 ((~ f),m)) )
ProjMap1 (f,m) is non-decreasing by A1;
hence ProjMap2 ((~ f),m) is non-decreasing by Th32; :: thesis: seq . m = lim (ProjMap2 ((~ f),m))
seq . m = lim (ProjMap1 (f,m)) by A1;
hence seq . m = lim (ProjMap2 ((~ f),m)) by Th32; :: thesis: verum
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 being 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 ; :: thesis: (lim_in_cod2 (Partial_Sums_in_cod2 (~ f))) . n = (lim_in_cod1 (Partial_Sums_in_cod1 f)) . n
(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 (lim_in_cod2 (Partial_Sums_in_cod2 (~ f))) . n = (lim_in_cod1 (Partial_Sums_in_cod1 f)) . n by D1DEF6; :: thesis: verum
end;
hence ( lim_in_cod1 (Partial_Sums_in_cod1 f) is non-decreasing & Sum seq = lim (lim_in_cod1 (Partial_Sums_in_cod1 f)) ) by A2, FUNCT_2:def 8; :: thesis: verum