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:90;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((f | X) * g) or x in dom (f * (X | g)) )
assume x in dom ((f | X) * g) ; :: thesis: x in dom (f * (X | g))
then A3: ( x in dom g & g . x in dom (f | X) ) by FUNCT_1:21;
then A4: ( g . x in X & g . x in dom f ) by A1, XBOOLE_0:def 4;
then A5: x in dom (X | g) by A3, FUNCT_1:85;
then g . x = (X | g) . x by FUNCT_1:85;
hence x in dom (f * (X | g)) by A4, A5, FUNCT_1:21; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f * (X | g)) or x in dom ((f | X) * g) )
assume x in dom (f * (X | g)) ; :: thesis: x in dom ((f | X) * g)
then ( x in dom (X | g) & (X | g) . x in dom f ) by FUNCT_1:21;
then A6: ( x in dom g & g . x in X & g . x in dom f ) by FUNCT_1:85;
then g . x in dom (f | X) by A1, XBOOLE_0:def 4;
hence x in dom ((f | X) * g) by A6, FUNCT_1:21; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom ((f | X) * g) implies ((f | X) * g) . x = (f * (X | g)) . x )
assume 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) & (f * (X | g)) . x = f . ((X | g) . x) & x in dom (X | g) ) by A2, FUNCT_1:21, FUNCT_1:22;
then ( ((f | X) * g) . x = f . (g . x) & (f * (X | g)) . x = f . (g . x) ) by FUNCT_1:70, FUNCT_1:85;
hence ((f | X) * g) . x = (f * (X | g)) . x ; :: thesis: verum

end;

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