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