the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def 2;
hence S1 +* S2 is finite ; :: thesis: verum