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 :: thesis: for x being object holds
( ( 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)) ) )
let x be object ; :: 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 A1: x in dom ((G | (F .: X)) * (F | X)) ; :: thesis: x in dom ((G * F) | X)
then A2: x in dom (F | X) by Th11;
then A3: x in (dom F) /\ X by RELAT_1:61;
then A4: x in X by XBOOLE_0:def 4;
(F | X) . x in dom (G | (F .: X)) by A1, Th11;
then F . x in dom (G | (F .: X)) by A2, Th46;
then F . x in (dom G) /\ (F .: X) by RELAT_1:61;
then A5: F . x in dom G by XBOOLE_0:def 4;
x in dom F by A3, XBOOLE_0:def 4;
then x in dom (G * F) by A5, Th11;
then x in (dom (G * F)) /\ X by A4, XBOOLE_0:def 4;
hence x in dom ((G * F) | X) by RELAT_1:61; :: thesis: verum
end;
assume x in dom ((G * F) | X) ; :: thesis: x in dom ((G | (F .: X)) * (F | X))
then A6: x in (dom (G * F)) /\ X by RELAT_1:61;
then A7: x in dom (G * F) by XBOOLE_0:def 4;
then A8: F . x in dom G by Th11;
A9: x in X by A6, XBOOLE_0:def 4;
x in dom F by A7, Th11;
then x in (dom F) /\ X by A9, XBOOLE_0:def 4;
then A10: x in dom (F | X) by RELAT_1:61;
x in dom F by A7, Th11;
then F . x in F .: X by A9, Def6;
then F . x in (dom G) /\ (F .: X) by A8, XBOOLE_0:def 4;
then F . x in dom (G | (F .: X)) by RELAT_1:61;
then (F | X) . x in dom (G | (F .: X)) by A10, Th46;
hence x in dom ((G | (F .: X)) * (F | X)) by A10, Th11; :: thesis: verum
end;
then A11: dom ((G * F) | X) = dom ((G | (F .: X)) * (F | X)) by TARSKI:2;
now :: thesis: for x being object st x in dom ((G * F) | X) holds
((G | (F .: X)) * (F | X)) . x = ((G * F) | X) . x
let x be object ; :: thesis: ( x in dom ((G * F) | X) implies ((G | (F .: X)) * (F | X)) . x = ((G * F) | X) . x )
assume A12: x in dom ((G * F) | X) ; :: thesis: ((G | (F .: X)) * (F | X)) . x = ((G * F) | X) . x
then A13: x in (dom (G * F)) /\ X by RELAT_1:61;
then x in dom (G * F) by XBOOLE_0:def 4;
then A14: x in dom F by Th11;
A15: x in X by A13, XBOOLE_0:def 4;
then A16: F . x in F .: X by A14, Def6;
thus ((G | (F .: X)) * (F | X)) . x = (G | (F .: X)) . ((F | X) . x) by A11, A12, Th12
.= (G | (F .: X)) . (F . x) by A15, Th48
.= G . (F . x) by A16, Th48
.= (G * F) . x by A14, Th13
.= ((G * F) | X) . x by A13, Th47 ; :: thesis: verum
end;
hence (G | (F .: X)) * (F | X) = (G * F) | X by A11; :: thesis: verum