set X = MSVars C;
consider m, a being OperSymbol of C such that
A1: the_result_sort_of m = a_Type and
A2: the_arity_of m = {} and
A3: the_result_sort_of a = an_Adj and
A4: the_arity_of a = {} by Def12;
A5: root-tree [m, the carrier of C] in the Sorts of (Free (C,(MSVars C))) . a_Type by A1, A2, MSAFREE3:5;
A6: root-tree [a, the carrier of C] in the Sorts of (Free (C,(MSVars C))) . an_Adj by A3, A4, MSAFREE3:5;
set x = the variable;
A7: a_Term C = a_Term ;
(MSVars C) . a_Term = Vars by Def25;
then A8: root-tree [ the variable,a_Term] in the Sorts of (Free (C,(MSVars C))) . a_Term by A7, MSAFREE3:4;
assume the Sorts of (Free (C,(MSVars C))) is V8() ; :: according to MSUALG_1:def 3 :: thesis: contradiction
then {} in rng the Sorts of (Free (C,(MSVars C))) by RELAT_1:def 9;
then consider s being object such that
A9: s in dom the Sorts of (Free (C,(MSVars C))) and
A10: {} = the Sorts of (Free (C,(MSVars C))) . s by FUNCT_1:def 3;
s in the carrier of C by A9;
then s in {a_Type,an_Adj,a_Term} by Def9;
hence contradiction by A5, A6, A8, A10, ENUMSET1:def 1; :: thesis: verum