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

A5: now :: thesis: for x, y being set st [x,y] in (dom m1) `1 holds
[(((m2 `2) * (m1 `2)) . x),(((m2 `2) * (m1 `2)) . y)] in (cod m2) `1

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:87;
then A7: x in dom (m1 `2) by A3, A4, FUNCT_2:def 1;
y in (dom m1) `2 by A6, ZFMISC_1:87;
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, Th42;
then [((m2 `2) . ((m1 `2) . x)),((m2 `2) . ((m1 `2) . y))] in (cod m2) `1 by A1, Th42;
then [(((m2 `2) * (m1 `2)) . x),((m2 `2) . ((m1 `2) . y))] in (cod m2) `1 by A7, FUNCT_1:13;
hence [(((m2 `2) * (m1 `2)) . x),(((m2 `2) * (m1 `2)) . y)] in (cod m2) `1 by A8, FUNCT_1:13; :: thesis: verum

end;

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