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