let S1, S2 be non empty finite ManySortedSign ; :: thesis: S1 +* S2 is finite
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as finite set ;
the carrier of (S1 +* S2) = C1 \/ C2 by Def2;
hence S1 +* S2 is finite ; :: thesis: verum