theorem Th15: :: FUNCT_2:15

for X, Y being set
for x being object
for f being Function of X,Y
for g being Function st Y <> {} & x in X holds
(g * f) . x = g . (f . x)