reconsider m = m as Nat by TARSKI:1;
set w = the 0wff string of S;
the 0wff string of S is 0 + (0 * m) -wff ;
then the 0wff string of S is 0 + m -wff ;
hence ex b₁ being string of S st b₁ is m -wff ; :: thesis: verum