let V be non empty set ; for m1, m2, m3 being Element of Maps V st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1
let m1, m2, m3 be Element of Maps V; ( dom m2 = cod m1 & dom m3 = cod m2 implies m3 * (m2 * m1) = (m3 * m2) * m1 )
assume that
A1:
dom m2 = cod m1
and
A2:
dom m3 = cod m2
; m3 * (m2 * m1) = (m3 * m2) * m1
A3:
cod (m2 * m1) = cod m2
by A1, Th12;
(m2 * m1) `2 = (m2 `2) * (m1 `2)
by A1, Th12;
then A4:
(m3 * (m2 * m1)) `2 = (m3 `2) * ((m2 `2) * (m1 `2))
by A2, A3, Th12;
A5:
dom (m3 * m2) = dom m2
by A2, Th12;
then A6:
dom ((m3 * m2) * m1) = dom m1
by A1, Th12;
dom (m2 * m1) = dom m1
by A1, Th12;
then A7:
dom (m3 * (m2 * m1)) = dom m1
by A2, A3, Th12;
cod (m3 * m2) = cod m3
by A2, Th12;
then A8:
cod ((m3 * m2) * m1) = cod m3
by A1, A5, Th12;
(m3 * m2) `2 = (m3 `2) * (m2 `2)
by A2, Th12;
then A9:
((m3 * m2) * m1) `2 = ((m3 `2) * (m2 `2)) * (m1 `2)
by A1, A5, Th12;
cod (m3 * (m2 * m1)) = cod m3
by A2, A3, Th12;
hence
m3 * (m2 * m1) = (m3 * m2) * m1
by A4, A7, A9, A6, A8, Lm2, RELAT_1:36; verum