set phi = the 0 -wff string of S;
set N = TheNorSymbOf S;
set phi1 = (<*(TheNorSymbOf S)*> ^ the 0 -wff string of S) ^ the 0 -wff string of S;
consider m being Nat such that
A1: m1 = m + 1 by NAT_1:6;
(<*(TheNorSymbOf S)*> ^ the 0 -wff string of S) ^ the 0 -wff string of S is non 0wff 1 + (0 * m) -wff string of S ;
then reconsider phi11 = (<*(TheNorSymbOf S)*> ^ the 0 -wff string of S) ^ the 0 -wff string of S as non 0wff m1 -wff string of S by A1;
take phi11 ; :: thesis: not phi11 is exal
thus not phi11 is exal ; :: thesis: verum