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 b_{1} being string of S st b_{1} = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds

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

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 b

b