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;