theorem Th9: :: TOPS_5:9

for I being 2 -element set
for f being ManySortedSet of I
for i, j being Element of I st i <> j holds
f = (i,j) --> ((f . i),(f . j))