let V be non empty set ; :: thesis: for m2, m1, m3 being Element of Maps V st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1
let m2, m1, 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
( (m2 * m1) `2 = (m2 `2 ) * (m1 `2 ) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 & (m3 * m2) `2 = (m3 `2 ) * (m2 `2 ) & dom (m3 * m2) = dom m2 & cod (m3 * m2) = cod m3 ) by A1, A2, Th12;
then ( (m3 * (m2 * m1)) `2 = (m3 `2 ) * ((m2 `2 ) * (m1 `2 )) & dom (m3 * (m2 * m1)) = dom m1 & cod (m3 * (m2 * m1)) = cod m3 & ((m3 * m2) * m1) `2 = ((m3 `2 ) * (m2 `2 )) * (m1 `2 ) & dom ((m3 * m2) * m1) = dom m1 & cod ((m3 * m2) * m1) = cod m3 & (m3 `2 ) * ((m2 `2 ) * (m1 `2 )) = ((m3 `2 ) * (m2 `2 )) * (m1 `2 ) ) by A1, A2, Th12, RELAT_1:55;
hence m3 * (m2 * m1) = (m3 * m2) * m1 by Lm2; :: thesis: verum