let S be non void Signature; :: thesis: for A being non-empty disjoint_valued MSAlgebra of S holds the Sorts of A is one-to-one
let A be non-empty disjoint_valued MSAlgebra of S; :: thesis: the Sorts of A is one-to-one
let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in dom the Sorts of A or not y in dom the Sorts of A or not the Sorts of A . x = the Sorts of A . y or x = y )
assume ( x in dom the Sorts of A & y in dom the Sorts of A ) ; :: thesis: ( not the Sorts of A . x = the Sorts of A . y or x = y )
then reconsider a = x, b = y as SortSymbol of S by PARTFUN1:def 4;
consider z being Element of the Sorts of A . a;
A1: the Sorts of A is disjoint_valued by MSAFREE1:def 2;
assume ( the Sorts of A . x = the Sorts of A . y & x <> y ) ; :: thesis: contradiction
then ( z in the Sorts of A . b & the Sorts of A . a misses the Sorts of A . b ) by A1, PROB_2:def 3;
hence contradiction by XBOOLE_0:3; :: thesis: verum