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 )
assume that
A1: f1 | X is Lipschitzian and
A2: f2 | X1 is Lipschitzian and
A3: f1 | Z is bounded and
A4: f2 | Z1 is bounded ; :: thesis: (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian
F: (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) = (f1 | (((X /\ Z) /\ X1) /\ Z1)) (#) (f2 | (((X /\ Z) /\ X1) /\ Z1)) by RFUNCT_1:61;
Y: 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:100 ;
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:100 ;
then X: ( f1 | (((X /\ Z) /\ X1) /\ Z1) is bounded & f1 | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian ) by Y, A1, A3;
Y: f2 | (((X /\ Z) /\ X1) /\ Z1) = (f2 | Z1) | ((X /\ Z) /\ X1) by RELAT_1:100;
f2 | (((X /\ Z) /\ X1) /\ Z1) = f2 | (((X /\ Z) /\ Z1) /\ X1) by XBOOLE_1:16
.= (f2 | X1) | ((Z /\ X) /\ Z1) by RELAT_1:100 ;
then ( f2 | (((X /\ Z) /\ X1) /\ Z1) is bounded & f2 | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian ) by Y, A2, A4;
hence (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian by X, F; :: thesis: verum