let X, Y be set ; :: thesis: for f1, f2 being real-valued Function st f1 | X is bounded & f2 | Y is bounded holds
( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
let f1, f2 be real-valued Function; :: thesis: ( f1 | X is bounded & f2 | Y is bounded implies ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) )
assume that
A1: f1 | X is bounded and
A2: f2 | Y is bounded ; :: thesis: ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
(f1 (#) f2) | (X /\ Y) = (f1 | (X /\ Y)) (#) (f2 | (X /\ Y)) by Th45
.= (f1 | (X /\ Y)) (#) ((f2 | Y) | X) by RELAT_1:71
.= ((f1 | X) | Y) (#) ((f2 | Y) | X) by RELAT_1:71 ;
hence (f1 (#) f2) | (X /\ Y) is bounded by A1, A2; :: thesis: (f1 - f2) | (X /\ Y) is bounded
(- f2) | Y is bounded by A2, Th82;
hence (f1 - f2) | (X /\ Y) is bounded by A1, Th83; :: thesis: verum