:: deftheorem Def6 defines * ENS_1:def 6 :
for V being non empty set
for m1, m2 being Element of Maps V st cod m1 = dom m2 holds
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];