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_{1} being set st b_{1} = ((S -firstChar) . phi) \+\ (TheNorSymbOf S) holds

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

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

b