let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: for seq being ExtREAL_sequence st ( for m being Element of NAT holds seq . m = lim_inf (ProjMap1 (f,m)) ) holds
Sum seq <= lim_inf (lim_in_cod1 (Partial_Sums_in_cod1 f))
let seq be ExtREAL_sequence; :: thesis: ( ( for m being Element of NAT holds seq . m = lim_inf (ProjMap1 (f,m)) ) implies Sum seq <= lim_inf (lim_in_cod1 (Partial_Sums_in_cod1 f)) )
assume A1: for m being Element of NAT holds seq . m = lim_inf (ProjMap1 (f,m)) ; :: thesis: Sum seq <= lim_inf (lim_in_cod1 (Partial_Sums_in_cod1 f))
now :: thesis: for m being Element of NAT holds seq . m = lim_inf (ProjMap2 ((~ f),m))
let m be Element of NAT ; :: thesis: seq . m = lim_inf (ProjMap2 ((~ f),m))
ProjMap1 (f,m) = ProjMap2 ((~ f),m) by Th32;
hence seq . m = lim_inf (ProjMap2 ((~ f),m)) by A1; :: thesis: verum
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; :: thesis: verum