let S1, S2 be non empty unsplit ManySortedSign ; :: thesis: S1 +* S2 is unsplit
set S = S1 +* S2;
A1: the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
A2: the ResultSort of S1 = id the carrier' of S1 by Def7;
A3: the ResultSort of S2 = id the carrier' of S2 by Def7;
the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
hence the ResultSort of (S1 +* S2) = id the carrier' of (S1 +* S2) by A1, A2, A3, FUNCT_4:22; :: according to CIRCCOMB:def 7 :: thesis: verum