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 Def25;
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 Def23;
ww in dom ((I,n) -TruthEval) by A2, Def24;
then ((I,n) -TruthEval) . ww = ((I,n) -TruthEval) /. ww by 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 Def23;
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 w in dom ((I,m) -TruthEval) by A3, Def24;
then A5: ((I,m) -TruthEval) . w = ((I,(m + n)) -TruthEval) . w by A4, GRFUNC_1:2;
ww in dom ((I,n) -TruthEval) by A2, Def24;
hence IT = ((I,m) -TruthEval) . w by A5, A4, GRFUNC_1:2; :: thesis: verum