let S be non empty ManySortedSign ; :: thesis: ( S is unsplit implies the carrier' of S c= the carrier of S )
assume A1: S is unsplit ; :: thesis: the carrier' of S c= the carrier of S
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of S or x in the carrier of S )
assume A2: x in the carrier' of S ; :: thesis: x in the carrier of S
then the ResultSort of S . x = x by A1, Th44;
hence x in the carrier of S by A2, FUNCT_2:5; :: thesis: verum