A1: (f #) * p is FinSequence of QuasiTerms C by Th130;
rng p c= Union the Sorts of (Free (C,(MSVars C))) ;
hence p at f is FinSequence of QuasiTerms C by A1, Def62; :: thesis: verum