theorem :: FUNCT_4:2

for f, g being Function holds g * f = (g | (rng f)) * f