let A be non empty closed_interval Subset of REAL; :: thesis: for f, g being PartFunc of REAL,REAL st f | A is bounded & g | A is bounded holds
(f (#) g) | A is bounded
let f, g be PartFunc of REAL,REAL; :: thesis: ( f | A is bounded & g | A is bounded implies (f (#) g) | A is bounded )
assume ( f | A is bounded & g | A is bounded ) ; :: thesis: (f (#) g) | A is bounded
then (f (#) g) | (A /\ A) is bounded by RFUNCT_1:84;
hence (f (#) g) | A is bounded ; :: thesis: verum