let X, X1, Z, Z1 be set ; 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; ( 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 )
; (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian
hence
(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian
by A1, A2, A4, A3; verum