let X, X1, Z, Z1 be set ; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded holds
(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded implies (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian )
A1: f1 | (((X /\ Z) /\ X1) /\ Z1) = f1 | ((X1 /\ Z1) /\ (X /\ Z)) by XBOOLE_1:16
.= f1 | (((X1 /\ Z1) /\ X) /\ Z) by XBOOLE_1:16
.= (f1 | Z) | ((X1 /\ Z1) /\ X) by RELAT_1:71 ;
A2: f1 | (((X /\ Z) /\ X1) /\ Z1) = f1 | ((X1 /\ Z1) /\ (X /\ Z)) by XBOOLE_1:16
.= f1 | (((X1 /\ Z1) /\ Z) /\ X) by XBOOLE_1:16
.= (f1 | X) | ((X1 /\ Z1) /\ Z) by RELAT_1:71 ;
A3: f2 | (((X /\ Z) /\ X1) /\ Z1) = f2 | (((X /\ Z) /\ Z1) /\ X1) by XBOOLE_1:16
.= (f2 | X1) | ((Z /\ X) /\ Z1) by RELAT_1:71 ;
A4: ( (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) = (f1 | (((X /\ Z) /\ X1) /\ Z1)) (#) (f2 | (((X /\ Z) /\ X1) /\ Z1)) & f2 | (((X /\ Z) /\ X1) /\ Z1) = (f2 | Z1) | ((X /\ Z) /\ X1) ) by RELAT_1:71, RFUNCT_1:45;
assume ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded ) ; :: thesis: (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian
hence (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian by A1, A2, A4, A3; :: thesis: verum