theorem MFG: :: RVSUM_4:3

for f, g being complex-valued Function
for X being set holds (f (#) g) | X = (f | X) (#) (g | X)