let X be set ; for m1, m2, m3 being Element of MapsT X st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1
let m1, m2, m3 be Element of MapsT X; ( 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, Th43;
(m2 * m1) `2 = (m2 `2) * (m1 `2)
by A1, Th43;
then A4:
(m3 * (m2 * m1)) `2 = (m3 `2) * ((m2 `2) * (m1 `2))
by A2, A3, Th43;
A5:
dom (m3 * m2) = dom m2
by A2, Th43;
then A6:
dom ((m3 * m2) * m1) = dom m1
by A1, Th43;
dom (m2 * m1) = dom m1
by A1, Th43;
then A7:
dom (m3 * (m2 * m1)) = dom m1
by A2, A3, Th43;
cod (m3 * m2) = cod m3
by A2, Th43;
then A8:
cod ((m3 * m2) * m1) = cod m3
by A1, A5, Th43;
(m3 * m2) `2 = (m3 `2) * (m2 `2)
by A2, Th43;
then A9:
((m3 * m2) * m1) `2 = ((m3 `2) * (m2 `2)) * (m1 `2)
by A1, A5, Th43;
cod (m3 * (m2 * m1)) = cod m3
by A2, A3, Th43;
hence
m3 * (m2 * m1) = (m3 * m2) * m1
by A4, A7, A9, A6, A8, Lm4, RELAT_1:36; verum