theorem Th52: :: FUNCT_7:53

for x being object
for f, g being Function holds apply (<*f,g*>,x) = <*x,(f . x),(g . (f . x))*>