let X be non empty set ; :: thesis: for Y, Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
for F1 being Function of X,Y
for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds
F1 + F2 is bounded
let Y, Z be non empty Subset of ExtREAL ; :: thesis: ( Y c= REAL & Z c= REAL implies for F1 being Function of X,Y
for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds
F1 + F2 is bounded )
assume A1: ( Y c= REAL & Z c= REAL ) ; :: thesis: for F1 being Function of X,Y
for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds
F1 + F2 is bounded
let F1 be Function of X,Y; :: thesis: for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds
F1 + F2 is bounded
let F2 be Function of X,Z; :: thesis: ( F1 is bounded & F2 is bounded implies F1 + F2 is bounded )
assume ( F1 is bounded & F2 is bounded ) ; :: thesis: F1 + F2 is bounded
then ( F1 + F2 is bounded_above & F1 + F2 is bounded_below ) by A1, Th49, Th50;
hence F1 + F2 is bounded ; :: thesis: verum