let X be non empty set ; :: thesis: for G being Function of X,ExtREAL st G is nonnegative holds
On G is nonnegative
let G be Function of X,ExtREAL; :: thesis: ( G is nonnegative implies On G is nonnegative )
assume A1: G is nonnegative ; :: thesis: On G is nonnegative
for n being Element of NAT holds 0. <= (On G) . n

proof

let n be Element of NAT ; :: thesis: 0. <= (On G) . n

per cases ( n in X or not n in X ) ;

suppose A2: n in X ; :: thesis: 0. <= (On G) . n

then (On G) . n = G . n by Def1;
hence 0. <= (On G) . n by A1, A2, SUPINF_2:39; :: thesis: verum

end;

suppose not n in X ; :: thesis: 0. <= (On G) . n

hence 0. <= (On G) . n by Def1; :: thesis: verum

end;

end;

end;

hence On G is nonnegative by SUPINF_2:39; :: thesis: verum