for f being 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 ) )