(x SubstWith u) . p = (x,u) -SymbolSubstIn p by Def22;
hence for b₁ being FinSequence st b₁ = (x SubstWith u) . p holds
b₁ is m -element ; :: thesis: verum