theorem Th53: :: FUNCT_7:54

for X being set
for f, g, h being Function holds compose (<*f,g,h*>,X) = ((h * g) * f) * (id X)