theorem Th34: :: TOPS_5:34

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