:: deftheorem defines -SymbolSubstIn FOMODEL0:def 21 :
for X, x, y being set
for p being b₁ -valued FinSequence holds (x,y) -SymbolSubstIn p = ((id X) +* (x,y)) * p;