set psi = (l1,l2) -SymbolSubstIn phi;

consider m being Nat such that

A1: phi is m -wff by FOMODEL2:def 25;

thus for b_{1} being string of S st b_{1} = (l1,l2) -SymbolSubstIn phi holds

b_{1} is wff
by A1; :: thesis: verum

consider m being Nat such that

A1: phi is m -wff by FOMODEL2:def 25;

thus for b

b