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

(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