let f, g be Function; :: thesis: for X being set holds (f | X) * g = f * (X |` g)
let X be set ; :: thesis: (f | X) * g = f * (X |` g)
A1: dom (f | X) = (dom f) /\ X by RELAT_1:61;
A2: dom ((f | X) * g) = dom (f * (X |` g))

proof

thus dom ((f | X) * g) c= dom (f * (X |` g)) :: according to XBOOLE_0:def 10 :: thesis: dom (f * (X |` g)) c= dom ((f | X) * g)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((f | X) * g) or x in dom (f * (X |` g)) )
assume A3: x in dom ((f | X) * g) ; :: thesis: x in dom (f * (X |` g))
then A4: x in dom g by FUNCT_1:11;
A5: g . x in dom (f | X) by A3, FUNCT_1:11;
then A6: g . x in dom f by A1, XBOOLE_0:def 4;
g . x in X by A1, A5, XBOOLE_0:def 4;
then A7: x in dom (X |` g) by A4, FUNCT_1:53;
then g . x = (X |` g) . x by FUNCT_1:53;
hence x in dom (f * (X |` g)) by A6, A7, FUNCT_1:11; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f * (X |` g)) or x in dom ((f | X) * g) )
assume A8: x in dom (f * (X |` g)) ; :: thesis: x in dom ((f | X) * g)
then A9: x in dom (X |` g) by FUNCT_1:11;
then A10: x in dom g by FUNCT_1:53;
(X |` g) . x in dom f by A8, FUNCT_1:11;
then A11: g . x in dom f by A9, FUNCT_1:53;
g . x in X by A9, FUNCT_1:53;
then g . x in dom (f | X) by A1, A11, XBOOLE_0:def 4;
hence x in dom ((f | X) * g) by A10, FUNCT_1:11; :: thesis: verum

end;

now :: thesis: for x being object st x in dom ((f | X) * g) holds
((f | X) * g) . x = (f * (X |` g)) . x

let x be object ; :: thesis: ( x in dom ((f | X) * g) implies ((f | X) * g) . x = (f * (X |` g)) . x )
assume A12: x in dom ((f | X) * g) ; :: thesis: ((f | X) * g) . x = (f * (X |` g)) . x
then ( ((f | X) * g) . x = (f | X) . (g . x) & g . x in dom (f | X) ) by FUNCT_1:11, FUNCT_1:12;
then A13: ((f | X) * g) . x = f . (g . x) by FUNCT_1:47;
( (f * (X |` g)) . x = f . ((X |` g) . x) & x in dom (X |` g) ) by A2, A12, FUNCT_1:11, FUNCT_1:12;
hence ((f | X) * g) . x = (f * (X |` g)) . x by A13, FUNCT_1:53; :: thesis: verum

end;

hence (f | X) * g = f * (X |` g) by A2, FUNCT_1:2; :: thesis: verum