t in QuasiTerms C by Def28;
then t at f in QuasiTerms C by Th129;
hence t at f is quasi-term of C by Th41; :: thesis: verum