theorem :: FUNCT_1:100

for F, G being Function
for X, X1 being set holds (G | X1) * (F | X) = (G * F) | (X /\ (F " X1))