let F, G be Function; :: thesis: for X, X1 being set holds (G | X1) * (F | X) = (G * F) | (X /\ (F " X1))
let X, X1 be set ; :: thesis: (G | X1) * (F | X) = (G * F) | (X /\ (F " X1))
set Y = dom ((G | X1) * (F | X));
now :: thesis: for x being object holds
( ( x in dom ((G * F) | (X /\ (F " X1))) implies x in dom ((G | X1) * (F | X)) ) & ( x in dom ((G | X1) * (F | X)) implies x in dom ((G * F) | (X /\ (F " X1))) ) )
let x be object ; :: thesis: ( ( x in dom ((G * F) | (X /\ (F " X1))) implies x in dom ((G | X1) * (F | X)) ) & ( x in dom ((G | X1) * (F | X)) implies x in dom ((G * F) | (X /\ (F " X1))) ) )
thus ( x in dom ((G * F) | (X /\ (F " X1))) implies x in dom ((G | X1) * (F | X)) ) :: thesis: ( x in dom ((G | X1) * (F | X)) implies x in dom ((G * F) | (X /\ (F " X1))) )
proof
assume x in dom ((G * F) | (X /\ (F " X1))) ; :: thesis: x in dom ((G | X1) * (F | X))
then A1: x in (dom (G * F)) /\ (X /\ (F " X1)) by RELAT_1:61;
then A2: x in dom (G * F) by XBOOLE_0:def 4;
A3: x in X /\ (F " X1) by A1, XBOOLE_0:def 4;
then A4: x in X by XBOOLE_0:def 4;
x in dom F by A2, Th11;
then x in (dom F) /\ X by A4, XBOOLE_0:def 4;
then A5: x in dom (F | X) by RELAT_1:61;
x in F " X1 by A3, XBOOLE_0:def 4;
then A6: F . x in X1 by Def7;
F . x in dom G by A2, Th11;
then F . x in (dom G) /\ X1 by A6, XBOOLE_0:def 4;
then F . x in dom (G | X1) by RELAT_1:61;
then (F | X) . x in dom (G | X1) by A5, Th46;
hence x in dom ((G | X1) * (F | X)) by A5, Th11; :: thesis: verum
end;
assume A7: x in dom ((G | X1) * (F | X)) ; :: thesis: x in dom ((G * F) | (X /\ (F " X1)))
then A8: x in dom (F | X) by Th11;
then A9: x in (dom F) /\ X by RELAT_1:61;
then A10: x in dom F by XBOOLE_0:def 4;
A11: x in X by A9, XBOOLE_0:def 4;
(F | X) . x in dom (G | X1) by A7, Th11;
then F . x in dom (G | X1) by A8, Th46;
then A12: F . x in (dom G) /\ X1 by RELAT_1:61;
then F . x in X1 by XBOOLE_0:def 4;
then x in F " X1 by A10, Def7;
then A13: x in X /\ (F " X1) by A11, XBOOLE_0:def 4;
F . x in dom G by A12, XBOOLE_0:def 4;
then x in dom (G * F) by A10, Th11;
then x in (dom (G * F)) /\ (X /\ (F " X1)) by A13, XBOOLE_0:def 4;
hence x in dom ((G * F) | (X /\ (F " X1))) by RELAT_1:61; :: thesis: verum
end;
then A14: dom ((G | X1) * (F | X)) = dom ((G * F) | (X /\ (F " X1))) by TARSKI:2;
now :: thesis: for x being object st x in dom ((G | X1) * (F | X)) holds
((G | X1) * (F | X)) . x = ((G * F) | (X /\ (F " X1))) . x
let x be object ; :: thesis: ( x in dom ((G | X1) * (F | X)) implies ((G | X1) * (F | X)) . x = ((G * F) | (X /\ (F " X1))) . x )
assume A15: x in dom ((G | X1) * (F | X)) ; :: thesis: ((G | X1) * (F | X)) . x = ((G * F) | (X /\ (F " X1))) . x
then A16: x in dom (F | X) by Th11;
then A17: x in (dom F) /\ X by RELAT_1:61;
then A18: x in dom F by XBOOLE_0:def 4;
A19: (F | X) . x in dom (G | X1) by A15, Th11;
then A20: F . x in dom (G | X1) by A16, Th46;
A21: x in X by A17, XBOOLE_0:def 4;
F . x in dom (G | X1) by A16, A19, Th46;
then F . x in (dom G) /\ X1 by RELAT_1:61;
then F . x in X1 by XBOOLE_0:def 4;
then x in F " X1 by A18, Def7;
then A22: x in X /\ (F " X1) by A21, XBOOLE_0:def 4;
thus ((G | X1) * (F | X)) . x = (G | X1) . ((F | X) . x) by A15, Th12
.= (G | X1) . (F . x) by A16, Th46
.= G . (F . x) by A20, Th46
.= (G * F) . x by A18, Th13
.= ((G * F) | (X /\ (F " X1))) . x by A22, Th48 ; :: thesis: verum
end;
hence (G | X1) * (F | X) = (G * F) | (X /\ (F " X1)) by A14; :: thesis: verum