let m be Nat; :: thesis: 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; :: thesis: 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 ; :: thesis: 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;

now :: thesis: for x being object st x in U -InterpretersOf S holds
f . x in Funcs ((S -formulasOfMaxDepth m),BOOLEAN)

let x be object ; :: thesis: ( x in U -InterpretersOf S implies f . x in Funcs ((S -formulasOfMaxDepth m),BOOLEAN) )
assume x in U -InterpretersOf S ; :: thesis: f . x in Funcs ((S -formulasOfMaxDepth m),BOOLEAN)
then reconsider Ix = x as Element of U -InterpretersOf S ;
reconsider g = f . Ix as Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN) ;
( g is BOOLEAN -valued & g = (Ix,m) -TruthEval ) ;
then ( g = g & dom g = S -formulasOfMaxDepth m & rng g c= BOOLEAN ) by Def27;
hence f . x in Funcs ((S -formulasOfMaxDepth m),BOOLEAN) by FUNCT_2:def 2; :: thesis: verum

end;

hence curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth m),BOOLEAN)) by FUNCT_2:3, A1; :: thesis: verum