:: deftheorem defines -SymbolSubstIn FOMODEL0:def 20 :
for x, y being set
for p being FinSequence holds (x,y) -SymbolSubstIn p = p +~ (x,y);