set h = head phi;
set t = tail phi;
set A = I -TruthEval phi;
set B = I -TruthEval (head phi);
set C = I -TruthEval (tail phi);
set RH = (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi));
set F = S -firstChar ;
set l = (S -firstChar) . phi;
set N = TheNorSymbOf S;
((S -firstChar) . phi) \+\ (TheNorSymbOf S) = {} ;
then (S -firstChar) . phi = TheNorSymbOf S by FOMODEL0:29;
then A1: phi = (<*(TheNorSymbOf S)*> ^ (head phi)) ^ (tail phi) by Th23;
(I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi

proof

per cases ( not (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0 or (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0 ) ;

suppose A2: not (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0 ; :: thesis: (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi

( not I -TruthEval (head phi) = 1 & not I -TruthEval (tail phi) = 1 ) by A2;
then ( I -TruthEval (head phi) = 0 & I -TruthEval (tail phi) = 0 ) by FOMODEL0:39;
hence (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi by A1, Lm37; :: thesis: verum

end;

suppose A3: (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0 ; :: thesis: (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi

then ( 1 - (I -TruthEval (head phi)) = 0 or 1 - (I -TruthEval (tail phi)) = 0 ) ;
then not I -TruthEval phi = 1 by A1, Lm37;
hence (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi by A3, FOMODEL0:39; :: thesis: verum

end;

end;

end;

hence for b₁ being set st b₁ = (I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) holds
b₁ is empty ; :: thesis: verum