let V be non empty set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum