theorem Th12: :: FUNCT_1:12

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