let V be non empty set ; :: thesis: for m being Element of Maps V holds
( dom (m `2 ) = dom m & rng (m `2 ) c= cod m )
let m be Element of Maps V; :: thesis: ( dom (m `2 ) = dom m & rng (m `2 ) c= cod m )
( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) ) by Th9;
hence ( dom (m `2 ) = dom m & rng (m `2 ) c= cod m ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum