theorem :: CIRCCOMB:10

for S1, S2 being non empty finite ManySortedSign holds S1 +* S2 is finite