let X be non empty set ; for Y, Z being non empty Subset of ExtREAL
for F being Function of X,Y
for G being Function of X,Z holds sup (F + G) <= (sup F) + (sup G)
let Y, Z be non empty Subset of ExtREAL; for F being Function of X,Y
for G being Function of X,Z holds sup (F + G) <= (sup F) + (sup G)
let F be Function of X,Y; for G being Function of X,Z holds sup (F + G) <= (sup F) + (sup G)
let G be Function of X,Z; sup (F + G) <= (sup F) + (sup G)
A1:
sup ((rng F) + (rng G)) <= (sup (rng F)) + (sup (rng G))
by Th7;
sup (F + G) <= sup ((rng F) + (rng G))
by Th15, XXREAL_2:59;
hence
sup (F + G) <= (sup F) + (sup G)
by A1, XXREAL_0:2; verum