set N = TheNorSymbOf S;
set IT = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
consider m being Nat such that
A1:
phi1 is m -wff
by Def24;
consider n being Nat such that
A2:
phi2 is n -wff
by Def24;
reconsider phi11 = phi1 as m + (0 * n) -wff string of S by A1;
reconsider phi22 = phi2 as n + (0 * m) -wff string of S by A2;
reconsider phi111 = phi11 as m + n -wff string of S ;
reconsider phi222 = phi22 as m + n -wff string of S ;
(<*(TheNorSymbOf S)*> ^ phi111) ^ phi222 is (m + n) + 1 -wff string of S
;
hence
for b1 being string of S st b1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b1 is wff
; verum