rng p c= X ;
hence for b₁ being FinSequence holds
( b₁ = (x,y) -SymbolSubstIn p iff b₁ = ((id X) +* (x,y)) * p ) by FUNCT_7:116; :: thesis: verum