A2: ( (cod m2) `2 <> {} or (dom m2) `2 = {} ) by Th44;
A3: ( (cod m1) `2 <> {} or (dom m1) `2 = {} ) by Th44;
A4: m1 `2 is Function of ((dom m1) `2 ),((cod m1) `2 ) by Th44;

A5: now

let x, y be set ; :: thesis: ( [x,y] in (dom m1) `1 implies [(((m2 `2 ) * (m1 `2 )) . x),(((m2 `2 ) * (m1 `2 )) . y)] in (cod m2) `1 )
assume A6: [x,y] in (dom m1) `1 ; :: thesis: [(((m2 `2 ) * (m1 `2 )) . x),(((m2 `2 ) * (m1 `2 )) . y)] in (cod m2) `1
then x in (dom m1) `2 by ZFMISC_1:106;
then A7: x in dom (m1 `2 ) by A3, A4, FUNCT_2:def 1;
y in (dom m1) `2 by A6, ZFMISC_1:106;
then A8: y in dom (m1 `2 ) by A3, A4, FUNCT_2:def 1;
[((m1 `2 ) . x),((m1 `2 ) . y)] in (cod m1) `1 by A6, Th44;
then [((m2 `2 ) . ((m1 `2 ) . x)),((m2 `2 ) . ((m1 `2 ) . y))] in (cod m2) `1 by A1, Th44;
then [(((m2 `2 ) * (m1 `2 )) . x),((m2 `2 ) . ((m1 `2 ) . y))] in (cod m2) `1 by A7, FUNCT_1:23;
hence [(((m2 `2 ) * (m1 `2 )) . x),(((m2 `2 ) * (m1 `2 )) . y)] in (cod m2) `1 by A8, FUNCT_1:23; :: thesis: verum

end;

m2 `2 is Function of ((dom m2) `2 ),((cod m2) `2 ) by Th44;
then (m2 `2 ) * (m1 `2 ) is Function of ((dom m1) `2 ),((cod m2) `2 ) by A1, A3, A4, FUNCT_2:19;
hence [[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))] is Element of MapsT X by A1, A3, A2, A5, Th42; :: thesis: verum