rng p c= Union the Sorts of (Free C,(MSVars C)) ;
hence for b₁ being FinSequence of QuasiTerms C holds
( b₁ = p at f iff b₁ = (f # ) * p ) by Def62; :: thesis: verum