let m be Nat; for S being Language
for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth m),BOOLEAN))
let S be Language; for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth m),BOOLEAN))
let U be non empty set ; curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth m),BOOLEAN))
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set Fm = (S,U) -TruthEval m;
set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set Phim = S -formulasOfMaxDepth m;
reconsider f = curry ((S,U) -TruthEval m) as Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by Lm11;
A1:
dom f = U -InterpretersOf S
by FUNCT_2:def 1;
hence
curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth m),BOOLEAN))
by FUNCT_2:3, A1; verum