let X be set ; :: thesis: for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
( (m2 * m1) `2 = (m2 `2 ) * (m1 `2 ) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )
let m2, m1 be Element of MapsT X; :: thesis: ( dom m2 = cod m1 implies ( (m2 * m1) `2 = (m2 `2 ) * (m1 `2 ) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) )
assume dom m2 = cod m1 ; :: thesis: ( (m2 * m1) `2 = (m2 `2 ) * (m1 `2 ) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )
then [[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))] = m2 * m1 by Def28
.= [[(dom (m2 * m1)),(cod (m2 * m1))],((m2 * m1) `2 )] by Th43 ;
hence ( (m2 * m1) `2 = (m2 `2 ) * (m1 `2 ) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) by Lm2, ZFMISC_1:33; :: thesis: verum