let mm be Element of NAT ; :: thesis: for S being Language
for U being non empty set holds curry (((S,U) -TruthEval) . mm) 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) . mm) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))
let U be non empty set ; :: thesis: curry (((S,U) -TruthEval) . mm) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))
set II = U -InterpretersOf S;
set AF = AtomicFormulasOf S;
set f = ((S,U) -TruthEval) . mm;
set SS = AllSymbolsOf S;
set F = (S,U) -TruthEval ;
reconsider g = curry (((S,U) -TruthEval) . mm) as Element of PFuncs ((U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))) by FUNCT_6:14;
set y = the Element of AtomicFormulasOf S;
reconsider Z = 0 as Element of NAT ;
dom (S -TruthEval U) = [:(U -InterpretersOf S),(AtomicFormulasOf S):] by FUNCT_2:def 1;
then A1: dom (((S,U) -TruthEval) . 0) = [:(U -InterpretersOf S),(AtomicFormulasOf S):] by Def19;

now :: thesis: for x being object st x in U -InterpretersOf S holds
x in dom g

let x be object ; :: thesis: ( x in U -InterpretersOf S implies x in dom g )
assume x in U -InterpretersOf S ; :: thesis: x in dom g
then [x, the Element of AtomicFormulasOf S] in dom (((S,U) -TruthEval) . 0) by A1, ZFMISC_1:87;
then [x, the Element of AtomicFormulasOf S] in dom ((S,U) -TruthEval 0) by Def20;
then [x, the Element of AtomicFormulasOf S] in dom ((S,U) -TruthEval (0 + mm)) by Lm7;
then [x, the Element of AtomicFormulasOf S] in dom (((S,U) -TruthEval) . mm) by Def20;
hence x in dom g by FUNCT_5:19; :: thesis: verum

end;

then ( U -InterpretersOf S c= dom g & dom g c= U -InterpretersOf S ) ;
then reconsider gg = g as total PartFunc of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by XBOOLE_0:def 10, PARTFUN1:def 2;
curry (((S,U) -TruthEval) . mm) = gg ;
hence curry (((S,U) -TruthEval) . mm) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) ; :: thesis: verum