let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for n being Element of NAT st f is nonnegative holds
( ProjMap1 (f,n) is nonnegative & ProjMap2 (f,n) is nonnegative )
let n be Element of NAT ; :: thesis: ( f is nonnegative implies ( ProjMap1 (f,n) is nonnegative & ProjMap2 (f,n) is nonnegative ) )
assume A1: f is nonnegative ; :: thesis: ( ProjMap1 (f,n) is nonnegative & ProjMap2 (f,n) is nonnegative )
now :: thesis: for m being object st m in dom (ProjMap1 (f,n)) holds
(ProjMap1 (f,n)) . m >= 0
let m be object ; :: thesis: ( m in dom (ProjMap1 (f,n)) implies (ProjMap1 (f,n)) . m >= 0 )
assume m in dom (ProjMap1 (f,n)) ; :: thesis: (ProjMap1 (f,n)) . m >= 0
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; :: thesis: verum
end;
hence ProjMap1 (f,n) is nonnegative by SUPINF_2:52; :: thesis: ProjMap2 (f,n) is nonnegative
now :: thesis: for m being object st m in dom (ProjMap2 (f,n)) holds
(ProjMap2 (f,n)) . m >= 0
let m be object ; :: thesis: ( m in dom (ProjMap2 (f,n)) implies (ProjMap2 (f,n)) . m >= 0 )
assume m in dom (ProjMap2 (f,n)) ; :: thesis: (ProjMap2 (f,n)) . m >= 0
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; :: thesis: verum
end;
hence ProjMap2 (f,n) is nonnegative by SUPINF_2:52; :: thesis: verum