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 ) ;
end;
end;
hence for b1 being set st b1 = (I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) holds
b1 is empty ; :: thesis: verum