t in QuasiTerms C by ELEMENT;
then t at f in QuasiTerms C by ThTr;
hence t at f is quasi-term of C by Th42; :: thesis: verum