set psi = (l1,l2) -SymbolSubstIn phi;
consider m being Nat such that
A1: phi is m -wff by FOMODEL2:def 25;
thus for b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn phi holds
b₁ is wff by A1; :: thesis: verum