let f, g be complex-valued Function; :: thesis: for X being set holds (f (#) g) | X = (f | X) (#) (g | X)
let X be set ; :: thesis: (f (#) g) | X = (f | X) (#) (g | X)
A1: ( dom (f | X) = (dom f) /\ X & dom (g | X) = (dom g) /\ X & dom ((f (#) g) | X) = (dom (f (#) g)) /\ X ) by RELAT_1:61;
A2: ( dom (f (#) g) = (dom f) /\ (dom g) & dom ((f | X) (#) (g | X)) = (dom (f | X)) /\ (dom (g | X)) ) by VALUED_1:def 4;
then A3: dom ((f (#) g) | X) = ((dom f) /\ (dom g)) /\ X by RELAT_1:61
.= ((dom f) /\ X) /\ ((dom g) /\ X) by XBOOLE_1:116 ;
for x being object st x in dom ((f (#) g) | X) holds
((f (#) g) | X) . x = ((f | X) (#) (g | X)) . x

proof

let x be object ; :: thesis: ( x in dom ((f (#) g) | X) implies ((f (#) g) | X) . x = ((f | X) (#) (g | X)) . x )
assume B1: x in dom ((f (#) g) | X) ; :: thesis: ((f (#) g) | X) . x = ((f | X) (#) (g | X)) . x
then ( x in dom f & x in dom g & x in X ) by A3, XBOOLE_0:def 4;
then ( x in dom (f | X) & x in dom (g | X) ) by RELAT_1:57;
then B3: ( (f | X) . x = f . x & (g | X) . x = g . x ) by FUNCT_1:47;
((f (#) g) | X) . x = (f (#) g) . x by B1, FUNCT_1:47
.= (f . x) * (g . x) by B1, A1, VALUED_1:def 4
.= ((f | X) (#) (g | X)) . x by B1, B3, A1, A2, A3, VALUED_1:def 4 ;
hence ((f (#) g) | X) . x = ((f | X) (#) (g | X)) . x ; :: thesis: verum

end;

hence (f (#) g) | X = (f | X) (#) (g | X) by A1, A3, VALUED_1:def 4; :: thesis: verum