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 H1( Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) -> Element of bool [:[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN:] = ((ExIterator $1) +* (NorIterator $1)) +* $1;
defpred S1[ set , Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN), set ] means $3 = H1($2);
A1:
for n being 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 S1[n,x,y]
proof
let n be
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 S1[n,x,y]let x be
Element of
PFuncs (
[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN);
ex y being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st S1[n,x,y]
reconsider yy =
H1(
x) as
Element of
PFuncs (
[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN)
by PARTFUN1:45;
take y =
yy;
S1[n,x,y]
thus
S1[
n,
x,
y]
;
verum
end;
consider f being sequence of (PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) such that
A2:
( f . 0 = Z & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A1);
take
f
; ( 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 A2; 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 A2; verum