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),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))
let S be Language; :: thesis: for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))
let U be non empty set ; :: thesis: curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set f = (S,U) -TruthEval mm;
set g = ((S,U) -TruthEval) . mm;
curry ((S,U) -TruthEval mm) = curry (((S,U) -TruthEval) . mm) by Def20;
hence curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by Lm10; :: thesis: verum