:: deftheorem Def10 defines * COH_SP:def 10 :
for X being set
for l1, l2 being Element of MapsC X st cod l1 = dom l2 holds
l2 * l1 = [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))];