theorem Th23: :: COH_SP:23

for X being set
for l1, l2, l3 being Element of MapsC X st dom l2 = cod l1 & dom l3 = cod l2 holds
l3 * (l2 * l1) = (l3 * l2) * l1