theorem Th20: :: COH_SP:20

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