let S be non empty ManySortedSign ; :: thesis: ( S is unsplit iff for o being object st o in the carrier' of S holds
the ResultSort of S . o = o )
thus ( S is unsplit implies for o being object st o in the carrier' of S holds
the ResultSort of S . o = o ) by FUNCT_1:17; :: thesis: ( ( for o being object st o in the carrier' of S holds
the ResultSort of S . o = o ) implies S is unsplit )
assume A1: for o being object 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:17; :: according to CIRCCOMB:def 7 :: thesis: verum