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

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