theorem Th1: :: CIRCCOMB:1

for A, B being set
for f being ManySortedSet of A
for g being ManySortedSet of B st f c= g holds
f # c= g #