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