the_arity_of c = {} by A1;
then A2: root-tree [c, the carrier of C] in the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of c) by MSAFREE3:5;
dom the Sorts of (Free (C,(MSVars C))) = the carrier of C by PARTFUN1:def 2;
then root-tree [c, the carrier of C] in Union the Sorts of (Free (C,(MSVars C))) by A2, CARD_5:2;
hence [c, the carrier of C] -tree {} is expression of C by TREES_4:20; :: thesis: verum