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 ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) by Th8;
then reconsider ff = (S,U) -TruthEval m as Function of [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN ;
A1: dom ff = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] 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 A1, ZFMISC_1:87;
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