let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: ( ( f is convergent_in_cod1 implies lim_in_cod1 f is nonnegative ) & ( f is convergent_in_cod2 implies lim_in_cod2 f is nonnegative ) )
hereby :: thesis: ( f is convergent_in_cod2 implies lim_in_cod2 f is nonnegative )
assume A2: f is convergent_in_cod1 ; :: thesis: lim_in_cod1 f is nonnegative
now :: thesis: for n being object st n in dom (lim_in_cod1 f) holds
(lim_in_cod1 f) . n >= 0
let n be object ; :: thesis: ( n in dom (lim_in_cod1 f) implies (lim_in_cod1 f) . n >= 0 )
assume n in dom (lim_in_cod1 f) ; :: thesis: (lim_in_cod1 f) . n >= 0
then reconsider n1 = n as Element of NAT ;
A4: (lim_in_cod1 f) . n = lim (ProjMap2 (f,n1)) by D1DEF5;
for k being Nat holds 0 <= (ProjMap2 (f,n1)) . k by SUPINF_2:51;
hence (lim_in_cod1 f) . n >= 0 by A2, A4, MESFUNC9:10; :: thesis: verum
end;
hence lim_in_cod1 f is nonnegative by SUPINF_2:52; :: thesis: verum
end;
assume A2: f is convergent_in_cod2 ; :: thesis: lim_in_cod2 f is nonnegative
now :: thesis: for n being object st n in dom (lim_in_cod2 f) holds
(lim_in_cod2 f) . n >= 0
let n be object ; :: thesis: ( n in dom (lim_in_cod2 f) implies (lim_in_cod2 f) . n >= 0 )
assume n in dom (lim_in_cod2 f) ; :: thesis: (lim_in_cod2 f) . n >= 0
then reconsider n1 = n as Element of NAT ;
A4: (lim_in_cod2 f) . n = lim (ProjMap1 (f,n1)) by D1DEF6;
for k being Nat holds 0 <= (ProjMap1 (f,n1)) . k by SUPINF_2:51;
hence (lim_in_cod2 f) . n >= 0 by A2, A4, MESFUNC9:10; :: thesis: verum
end;
hence lim_in_cod2 f is nonnegative by SUPINF_2:52; :: thesis: verum