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

( (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