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))

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)

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;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) )
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;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

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

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

((f | X) * g) . x = (f * (X |` g)) . x

hence
(f | X) * g = f * (X |` g)
by A2, FUNCT_1:2; :: thesis: verum((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;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