:: deftheorem Def22 defines SubstWith FOMODEL0:def 22 :
for U being non empty set
for x being set
for u being Element of U
for b₄ being Function of (U *),(U *) holds
( b₄ = x SubstWith u iff for q being b₁ -valued FinSequence holds b₄ . q = (x,u) -SymbolSubstIn q );