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

let x be set ; :: 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 x in (dom (G * F)) /\ (X /\ (F " X1)) by RELAT_1:90;
then ( x in dom (G * F) & x in X /\ (F " X1) ) by XBOOLE_0:def 4;
then ( x in dom F & F . x in dom G & x in X & x in F " X1 ) by Th21, XBOOLE_0:def 4;
then ( x in dom F & F . x in dom G & x in X & F . x in X1 ) by Def13;
then ( x in (dom F) /\ X & F . x in (dom G) /\ X1 ) by XBOOLE_0:def 4;
then ( x in dom (F | X) & F . x in dom (G | X1) ) by RELAT_1:90;
then ( x in dom (F | X) & (F | X) . x in dom (G | X1) ) by Th70;
hence x in dom ((G | X1) * (F | X)) by Th21; :: thesis: verum

end;

assume x in dom ((G | X1) * (F | X)) ; :: thesis: x in dom ((G * F) | (X /\ (F " X1)))
then ( x in dom (F | X) & (F | X) . x in dom (G | X1) ) by Th21;
then ( x in (dom F) /\ X & F . x in dom (G | X1) ) by Th70, RELAT_1:90;
then ( x in (dom F) /\ X & F . x in (dom G) /\ X1 ) by RELAT_1:90;
then ( x in dom F & x in X & F . x in dom G & F . x in X1 ) by XBOOLE_0:def 4;
then ( x in dom (G * F) & x in X & x in F " X1 ) by Th21, Def13;
then ( x in dom (G * F) & x in X /\ (F " X1) ) by XBOOLE_0:def 4;
then x in (dom (G * F)) /\ (X /\ (F " X1)) by XBOOLE_0:def 4;
hence x in dom ((G * F) | (X /\ (F " X1))) by RELAT_1:90; :: thesis: verum

end;

then A1: dom ((G | X1) * (F | X)) = dom ((G * F) | (X /\ (F " X1))) by TARSKI:2;

now

let x be set ; :: thesis: ( x in dom ((G | X1) * (F | X)) implies ((G | X1) * (F | X)) . x = ((G * F) | (X /\ (F " X1))) . x )
assume A2: x in dom ((G | X1) * (F | X)) ; :: thesis: ((G | X1) * (F | X)) . x = ((G * F) | (X /\ (F " X1))) . x
then A3: ( x in dom (F | X) & (F | X) . x in dom (G | X1) ) by Th21;
then A4: ( x in dom (F | X) & F . x in dom (G | X1) ) by Th70;
( x in (dom F) /\ X & F . x in dom (G | X1) ) by A3, Th70, RELAT_1:90;
then A5: ( x in dom F & x in X & F . x in (dom G) /\ X1 ) by RELAT_1:90, XBOOLE_0:def 4;
then ( x in dom F & x in X & F . x in dom G & F . x in X1 ) by XBOOLE_0:def 4;
then ( x in dom (G * F) & x in X & x in F " X1 ) by Th21, Def13;
then A6: ( x in dom (G * F) & x in X /\ (F " X1) ) by XBOOLE_0:def 4;
thus ((G | X1) * (F | X)) . x = (G | X1) . ((F | X) . x) by A2, Th22
.= (G | X1) . (F . x) by A3, Th70
.= G . (F . x) by A4, Th70
.= (G * F) . x by A5, Th23
.= ((G * F) | (X /\ (F " X1))) . x by A6, Th72 ; :: thesis: verum

end;

hence (G | X1) * (F | X) = (G * F) | (X /\ (F " X1)) by A1, Th9; :: thesis: verum