consider m being Nat such that
A1: phi is m -wff by Def24;
reconsider phii = phi as m -wff string of S by A1;
set IT = <*l*> ^ phii;
<*l*> ^ phii is m + 1 -wff ;
hence for b₁ being string of S st b₁ = <*l*> ^ phi holds
b₁ is wff ; :: thesis: verum