let S be non empty ManySortedSign ; :: thesis: ( SingleAlg S is non-empty & SingleAlg S is disjoint_valued )
set F = the Sorts of (SingleAlg S);

hereby :: according to MSUALG_1:def 3,PBOOLE:def 13 :: thesis: SingleAlg S is disjoint_valued

let x be object ; :: thesis: ( x in the carrier of S implies not the Sorts of (SingleAlg S) . x is empty )
assume x in the carrier of S ; :: thesis: not the Sorts of (SingleAlg S) . x is empty
then the Sorts of (SingleAlg S) . x = {x} by Def3;
hence not the Sorts of (SingleAlg S) . x is empty ; :: thesis: verum

end;

let x, y be object ; :: according to PROB_2:def 2,MSAFREE1:def 2 :: thesis: ( x = y or the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y )
assume A1: x <> y ; :: thesis: the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y

per cases ( ( x in dom the Sorts of (SingleAlg S) & y in dom the Sorts of (SingleAlg S) ) or not x in dom the Sorts of (SingleAlg S) or not y in dom the Sorts of (SingleAlg S) ) ;

suppose A2: ( x in dom the Sorts of (SingleAlg S) & y in dom the Sorts of (SingleAlg S) ) ; :: thesis: the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y

dom the Sorts of (SingleAlg S) = the carrier of S by PARTFUN1:def 2;
then A3: ( the Sorts of (SingleAlg S) . x = {x} & the Sorts of (SingleAlg S) . y = {y} ) by A2, Def3;
assume the Sorts of (SingleAlg S) . x meets the Sorts of (SingleAlg S) . y ; :: thesis: contradiction
hence contradiction by A1, A3, ZFMISC_1:11; :: thesis: verum

end;

suppose ( not x in dom the Sorts of (SingleAlg S) or not y in dom the Sorts of (SingleAlg S) ) ; :: thesis: the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y

then ( the Sorts of (SingleAlg S) . x = {} or the Sorts of (SingleAlg S) . y = {} ) by FUNCT_1:def 2;
hence the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y by XBOOLE_1:65; :: thesis: verum

end;

end;