let S be non empty ManySortedSign ; :: thesis: ( S is unsplit iff for o being set st o in the carrier' of S holds
the ResultSort of S . o = o )

hereby :: thesis: ( ( for o being set st o in the carrier' of S holds
the ResultSort of S . o = o ) implies S is unsplit )

assume S is unsplit ; :: thesis: for o being set st o in the carrier' of S holds
the ResultSort of S . o = o
then the ResultSort of S = id the carrier' of S by Def7;
hence for o being set st o in the carrier' of S holds
the ResultSort of S . o = o by FUNCT_1:34; :: thesis: verum

end;

assume A1: for o being set st o in the carrier' of S holds
the ResultSort of S . o = o ; :: thesis: S is unsplit
dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
hence the ResultSort of S = id the carrier' of S by A1, FUNCT_1:34; :: according to CIRCCOMB:def 7 :: thesis: verum