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:19;
hence [[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))] is Element of Maps V by A1, A3, A2, Th5; :: thesis: verum