let m be Nat; :: thesis: for S being Language
for w being string of S
for U being non empty set
for I being Element of U -InterpretersOf S st w is m -wff holds
((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . [I,w]

let S be Language; :: thesis: for w being string of S
for U being non empty set
for I being Element of U -InterpretersOf S st w is m -wff holds
((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . [I,w]

let w be string of S; :: thesis: for U being non empty set
for I being Element of U -InterpretersOf S st w is m -wff holds
((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . [I,w]

let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S st w is m -wff holds
((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . [I,w]

set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: ( w is m -wff implies ((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . [I,w] )
set g = (I,m) -TruthEval ;
set f = (S,U) -TruthEval m;
set Phim = S -formulasOfMaxDepth m;
(S,U) -TruthEval m is Element of Funcs ([:(),():],BOOLEAN) by Th8;
then reconsider ff = (S,U) -TruthEval m as Function of [:(),():],BOOLEAN ;
A1: dom ff = [:(),():] by FUNCT_2:def 1;
assume w is m -wff ; :: thesis: ((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . [I,w]
then w in S -formulasOfMaxDepth m ;
then ( [I,w] in dom ((S,U) -TruthEval m) & (I,m) -TruthEval = (curry ((S,U) -TruthEval m)) . I ) by ;
then ( w in dom ((I,m) -TruthEval) & ((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . (I,w) ) by FUNCT_5:20;
hence ((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . [I,w] ; :: thesis: verum