let m be Nat; :: thesis: for S being Language
for U being non empty set holds
( (S,U) -TruthEval m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) & ((S,U) -TruthEval) . m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) )
let S be Language; :: thesis: for U being non empty set holds
( (S,U) -TruthEval m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) & ((S,U) -TruthEval) . m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) )
let U be non empty set ; :: thesis: ( (S,U) -TruthEval m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) & ((S,U) -TruthEval) . m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) )
set Fm = (S,U) -TruthEval m;
set II = U -InterpretersOf S;
set Phim = S -formulasOfMaxDepth m;
set SS = AllSymbolsOf S;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
reconsider Fmm = (S,U) -TruthEval m as PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN ;
dom ((S,U) -TruthEval m) c= [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] ;
then A1: uncurry (curry ((S,U) -TruthEval m)) = (S,U) -TruthEval m by FUNCT_5:50;
reconsider f = curry ((S,U) -TruthEval m) as Function of (U -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth m),BOOLEAN)) by Lm17;
( rng f c= Funcs ((S -formulasOfMaxDepth m),BOOLEAN) & dom f = U -InterpretersOf S ) by FUNCT_2:def 1;
then ( (S,U) -TruthEval m = (S,U) -TruthEval m & dom ((S,U) -TruthEval m) = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & rng ((S,U) -TruthEval m) c= BOOLEAN ) by A1, FUNCT_5:26;
hence (S,U) -TruthEval m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) by FUNCT_2:def 2; :: thesis: ((S,U) -TruthEval) . m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN)
then ((S,U) -TruthEval) . mm in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) by Def20;
hence ((S,U) -TruthEval) . m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) ; :: thesis: verum