let m be Nat; :: thesis: for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval in Funcs ((S -formulasOfMaxDepth m),BOOLEAN)
let S be Language; :: thesis: for U being non empty set
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval in Funcs ((S -formulasOfMaxDepth m),BOOLEAN)
let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S holds (I,m) -TruthEval in Funcs ((S -formulasOfMaxDepth m),BOOLEAN)
set Phim = S -formulasOfMaxDepth m;
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: (I,m) -TruthEval in Funcs ((S -formulasOfMaxDepth m),BOOLEAN)
reconsider F = curry ((S,U) -TruthEval m) as Function of (U -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth m),BOOLEAN)) by Lm17;
F . I in Funcs ((S -formulasOfMaxDepth m),BOOLEAN) ;
hence (I,m) -TruthEval in Funcs ((S -formulasOfMaxDepth m),BOOLEAN) ; :: thesis: verum