theorem Th13: :: FUNCT_1:13

for x being object
for f, g being Function st x in dom f holds
(g * f) . x = g . (f . x)