theorem :: CIRCCOMB:6

for S1, S2, S3 being non empty ManySortedSign holds (S1 +* S2) +* S3 = S1 +* (S2 +* S3)