let F, G be Function; :: thesis: for X being set holds (G | (F .: X)) * (F | X) = (G * F) | X
let X be set ; :: thesis: (G | (F .: X)) * (F | X) = (G * F) | X
set Y = dom ((G * F) | X);

now

let x be set ; :: thesis: ( ( x in dom ((G | (F .: X)) * (F | X)) implies x in dom ((G * F) | X) ) & ( x in dom ((G * F) | X) implies x in dom ((G | (F .: X)) * (F | X)) ) )
thus ( x in dom ((G | (F .: X)) * (F | X)) implies x in dom ((G * F) | X) ) :: thesis: ( x in dom ((G * F) | X) implies x in dom ((G | (F .: X)) * (F | X)) )

proof

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

end;

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

end;

then A4: dom ((G * F) | X) = dom ((G | (F .: X)) * (F | X)) by TARSKI:2;

now

let x be set ; :: thesis: ( x in dom ((G * F) | X) implies ((G | (F .: X)) * (F | X)) . x = ((G * F) | X) . x )
assume A5: x in dom ((G * F) | X) ; :: thesis: ((G | (F .: X)) * (F | X)) . x = ((G * F) | X) . x
then A6: x in (dom (G * F)) /\ X by RELAT_1:90;
then A7: ( x in dom (G * F) & x in X ) by XBOOLE_0:def 4;
then A8: ( x in dom F & F . x in dom G & x in X ) by Th21;
then A9: ( F . x in F .: X & F . x in dom G ) by Def12;
thus ((G | (F .: X)) * (F | X)) . x = (G | (F .: X)) . ((F | X) . x) by A4, A5, Th22
.= (G | (F .: X)) . (F . x) by A7, Th72
.= G . (F . x) by A9, Th72
.= (G * F) . x by A8, Th23
.= ((G * F) | X) . x by A6, Th71 ; :: thesis: verum

end;

hence (G | (F .: X)) * (F | X) = (G * F) | X by A4, Th9; :: thesis: verum