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