theorem Th21: :: MONOID_1:21

for D being non empty set
for G being non empty multMagma
for f1, f2 being Element of (.: (G,D))
for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a)