theorem sa: :: VECTSP13:35

for X being non empty set
for L being non empty associative multLoopStr
for a, b being Element of L
for f being Function of X,L holds (a * b) '*' f = a '*' (b '*' f)