set IU = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set III = I;
set II = I;
consider n being Nat such that
A1: w is n -wff by Def24;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
set fn = (I,n) -TruthEval ;
reconsider ww = w as n -wff string of S by A1;
A2: S -formulasOfMaxDepth nn = dom ((I,nn) -TruthEval) by Def22;
((I,n) -TruthEval) . ww = ((I,n) -TruthEval) /. ww by A2, Def23, PARTFUN1:def 6;
then reconsider IT = ((I,n) -TruthEval) . ww as Element of BOOLEAN ;
take IT ; :: thesis: for m being Nat st w is m -wff holds
IT = ((I,m) -TruthEval) . w
let m be Nat; :: thesis: ( w is m -wff implies IT = ((I,m) -TruthEval) . w )
set fm = (I,m) -TruthEval ;
set f = (I,(m + n)) -TruthEval ;
set g = (I,(n + m)) -TruthEval ;
reconsider mm = m, nn = n as Element of NAT by ORDINAL1:def 12;
A3: ( S -formulasOfMaxDepth m = dom ((I,mm) -TruthEval) & S -formulasOfMaxDepth nn = dom ((I,nn) -TruthEval) ) by Def22;
A4: ( (I,m) -TruthEval c= (I,(m + n)) -TruthEval & (I,n) -TruthEval c= (I,(n + m)) -TruthEval & (I,(m + n)) -TruthEval = (I,(n + m)) -TruthEval ) by Lm12;
assume w is m -wff ; :: thesis: IT = ((I,m) -TruthEval) . w
then ((I,m) -TruthEval) . w = ((I,(m + n)) -TruthEval) . w by A4, A3, GRFUNC_1:2;
hence IT = ((I,m) -TruthEval) . w by A2, Def23, A4, GRFUNC_1:2; :: thesis: verum