theorem Th12: :: ENS_1:12

for V being non empty set
for m1, m2 being Element of Maps V st dom m2 = cod m1 holds
( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )