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 )
A1: m `2 is Function of (dom m),(cod m) by Th9;
( cod m <> {} or dom m = {} ) by Th9;
hence ( dom (m `2) = dom m & rng (m `2) c= cod m ) by A1, FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum