A2: ( cod m2 <> {} or dom m2 = {} ) by Th9;
A3: ( cod m1 <> {} or dom m1 = {} ) by Th9;
( m1 `2 is Function of (dom m1),(cod m1) & m2 `2 is Function of (dom m2),(cod m2) ) by Th9;
then (m2 `2) * (m1 `2) is Function of (dom m1),(cod m2) by A1, A3, FUNCT_2:13;
hence [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of Maps V by A1, A3, A2, Th5; :: thesis: verum