let X be set ; :: thesis: for l2, l1 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 l2, l1 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 Def13
.= [[(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, ZFMISC_1:33; :: thesis: verum