set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set AF = AtomicFormulasOf S;
set Strings = ((AllSymbolsOf S) *) \ {{}};
set D = [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):];
reconsider ii = U -InterpretersOf S as Subset of (U -InterpretersOf S) by XBOOLE_0:def 10;
reconsider subboolean = BOOLEAN as Subset of BOOLEAN by XBOOLE_0:def 10;
reconsider sub = [:ii,(AtomicFormulasOf S):] as Subset of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] ;
[:sub,subboolean:] c= [:[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN:] ;
then S -TruthEval U is PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN by XBOOLE_1:1;
then reconsider Z = S -TruthEval U as Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) by PARTFUN1:45;
deffunc H₁( Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) -> Element of bool [:[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN:] = ((ExIterator $1) +* (NorIterator $1)) +* $1;
defpred S₁[ set , Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN), set ] means $3 = H₁($2);
B1: for n being Element of NAT
for x being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) ex y being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) ex y being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st S₁[n,x,y]
let x be Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN); :: thesis: ex y being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st S₁[n,x,y]
reconsider yy = H₁(x) as Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) by PARTFUN1:45;
take y = yy; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

consider f being Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) such that
B2: ( f . 0 = Z & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(B1);
take f ; :: thesis: ( f . 0 = S -TruthEval U & ( for mm being Element of NAT holds f . (mm + 1) = ((ExIterator (f . mm)) +* (NorIterator (f . mm))) +* (f . mm) ) )
thus f . 0 = S -TruthEval U by B2; :: thesis: for mm being Element of NAT holds f . (mm + 1) = ((ExIterator (f . mm)) +* (NorIterator (f . mm))) +* (f . mm)
thus for mm being Element of NAT holds f . (mm + 1) = ((ExIterator (f . mm)) +* (NorIterator (f . mm))) +* (f . mm) by B2; :: thesis: verum