let X be non empty set ; :: thesis: for G being Function of X,ExtREAL st G is V99() holds
On G is V99()
let G be Function of X,ExtREAL; :: thesis: ( G is V99() implies On G is V99() )
assume A1: G is V99() ; :: thesis: On G is V99()
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 V99() by SUPINF_2:39; :: thesis: verum