let X be set ; :: thesis: for l1, l2 being Element of MapsC X st dom l2 = cod l1 holds
( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 )
let l1, l2 be Element of MapsC X; :: thesis: ( dom l2 = cod l1 implies ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 ) )
assume dom l2 = cod l1 ; :: thesis: ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 )
then [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] = l2 * l1 by Def10
.= [[(dom (l2 * l1)),(cod (l2 * l1))],((l2 * l1) `2)] by Th20 ;
hence ( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 ) by Lm2, XTUPLE_0:1; :: thesis: verum