set F = S -firstChar ;
set N = TheNorSymbOf S;
set s = (S -firstChar) . phi;
consider m being Nat such that
A1: Depth phi = m + 1 by NAT_1:6;
phi in m -NorFormulasOf S by A1, Lm29;
then consider phi11, phi22 being Element of S -formulasOfMaxDepth m such that
A2: phi = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 ;
(S -firstChar) . phi = phi . 1 by FOMODEL0:6
.= (<*(TheNorSymbOf S)*> ^ (phi11 ^ phi22)) . 1 by A2, FINSEQ_1:32
.= TheNorSymbOf S by FINSEQ_1:41 ;
hence for b₁ being set st b₁ = ((S -firstChar) . phi) \+\ (TheNorSymbOf S) holds
b₁ is empty ; :: thesis: verum