theorem Th9: :: CIRCCOMB:9

for S1, S2 being non empty ManySortedSign st ( not S1 is void or not S2 is void ) holds
not S1 +* S2 is void