theorem Th9: :: ENS_1:9

for V being non empty set
for m being Element of Maps V holds
( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) )