theorem Th8: :: ENS_1:8

for V being non empty set
for m being Element of Maps V holds m = [[(dom m),(cod m)],(m `2)]