let X be set ; :: thesis: for l1, l2, l3 being Element of MapsC X st dom l2 = cod l1 & dom l3 = cod l2 holds
l3 * (l2 * l1) = (l3 * l2) * l1
let l1, l2, l3 be Element of MapsC X; :: thesis: ( dom l2 = cod l1 & dom l3 = cod l2 implies l3 * (l2 * l1) = (l3 * l2) * l1 )
assume that
A1: dom l2 = cod l1 and
A2: dom l3 = cod l2 ; :: thesis: l3 * (l2 * l1) = (l3 * l2) * l1
A3: cod (l2 * l1) = cod l2 by A1, Th22;
(l2 * l1) `2 = (l2 `2) * (l1 `2) by A1, Th22;
then A4: (l3 * (l2 * l1)) `2 = (l3 `2) * ((l2 `2) * (l1 `2)) by A2, A3, Th22;
A5: dom (l3 * l2) = dom l2 by A2, Th22;
then A6: dom ((l3 * l2) * l1) = dom l1 by A1, Th22;
dom (l2 * l1) = dom l1 by A1, Th22;
then A7: dom (l3 * (l2 * l1)) = dom l1 by A2, A3, Th22;
cod (l3 * l2) = cod l3 by A2, Th22;
then A8: cod ((l3 * l2) * l1) = cod l3 by A1, A5, Th22;
(l3 * l2) `2 = (l3 `2) * (l2 `2) by A2, Th22;
then A9: ((l3 * l2) * l1) `2 = ((l3 `2) * (l2 `2)) * (l1 `2) by A1, A5, Th22;
cod (l3 * (l2 * l1)) = cod l3 by A2, A3, Th22;
hence l3 * (l2 * l1) = (l3 * l2) * l1 by A4, A7, A9, A6, A8, Lm1, RELAT_1:36; :: thesis: verum