:: deftheorem Def23 defines * COH_SP:def 24 :
for X being set
for m1, m2 being Element of MapsT X st cod m1 = dom m2 holds
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];