set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
curry ((S,U) -TruthEval mm) = curry (((S,U) -TruthEval) . mm) by Def20;
then reconsider f = curry ((S,U) -TruthEval mm) as Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by Lm10;
f . I is Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN) ;
hence (curry ((S,U) -TruthEval m)) . I is Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN) ; :: thesis: verum