a in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by Def28;
then a at f in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by Th129;
hence a at f is expression of C, an_Adj C by Th41; :: thesis: verum