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