theorem Th41: :: COH_SP:42

for X being set
for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2)]