theorem :: PARTFUN1:36

for X, Y, Z being set
for f, g being Function st (rng f) /\ (dom g) c= Y holds
<:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:>