theorem Th22: :: COH_SP:22

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