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 ;
then A6: g . x in dom f by ;
g . x in X by ;
then A7: x in dom (X |` g) by ;
then g . x = (X |` g) . x by FUNCT_1:53;
hence x in dom (f * (X |` g)) by ; :: 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 ;
then A11: g . x in dom f by ;
g . x in X by ;
then g . x in dom (f | X) by ;
hence x in dom ((f | X) * g) by ; :: 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 ;
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 ;
hence ((f | X) * g) . x = (f * (X |` g)) . x by ; :: thesis: verum
end;
hence (f | X) * g = f * (X |` g) by ; :: thesis: verum