theorem Th1: :: MSUHOM_1:1

for f, g being Function
for C being set st rng f c= C holds
(g | C) * f = g * f