A1: Free (S,X) = FreeMSA X by MSAFREE3:31;
hence Free (S,X) is non-empty ; :: thesis: Free (S,X) is disjoint_valued
let x, y be object ; :: according to PROB_2:def 2,MSAFREE1:def 2 :: thesis: ( x = y or the Sorts of (Free (S,X)) . x misses the Sorts of (Free (S,X)) . y )
assume A2: x <> y ; :: thesis: the Sorts of (Free (S,X)) . x misses the Sorts of (Free (S,X)) . y
assume the Sorts of (Free (S,X)) . x meets the Sorts of (Free (S,X)) . y ; :: thesis: contradiction
then consider z being object such that
A3: ( z in the Sorts of (Free (S,X)) . x & z in the Sorts of (Free (S,X)) . y ) by XBOOLE_0:3;
A4: dom the Sorts of (Free (S,X)) = the carrier of S by PARTFUN1:def 2;
then reconsider x = x, y = y as SortSymbol of S by A3, FUNCT_1:def 2;
z in the Sorts of (Free (S,X)) . x by A3;
then reconsider z = z as Element of Union the Sorts of (Free (S,X)) by A4, CARD_5:2;
reconsider z = z as Term of S,X by A1, MSAFREE3:6;
( the_sort_of z = x & the_sort_of z = y ) by A1, A3, MSAFREE3:7;
hence contradiction by A2; :: thesis: verum