theorem Th44: :: CIRCCOMB:44

for S being non empty ManySortedSign holds
( S is unsplit iff for o being object st o in the carrier' of S holds
the ResultSort of S . o = o )