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

( 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