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 (inf F) + (inf G) <= inf (F + 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 (inf F) + (inf G) <= inf (F + G)
let F be Function of X,Y; :: thesis: for G being Function of X,Z holds (inf F) + (inf G) <= inf (F + G)
let G be Function of X,Z; :: thesis: (inf F) + (inf G) <= inf (F + G)
A3: inf ((rng F) + (rng G)) <= inf (F + G) by Th34, XXREAL_2:60;
(inf (rng F)) + (inf (rng G)) <= inf ((rng F) + (rng G)) by Th27;
hence (inf F) + (inf G) <= inf (F + G) by A3, XXREAL_0:2; :: thesis: verum