let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: for G being Function of X,Z holds sup (F + G) <= (sup F) + (sup G)

let G be Function of X,Z; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: for G being Function of X,Z holds sup (F + G) <= (sup F) + (sup G)

let G be Function of X,Z; :: thesis: 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; :: thesis: verum