theorem Th35: :: PARTFUN1:35

for X, Y, Z being set
for f, g being Function holds <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:>