set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set AF = AtomicFormulasOf S;
set Strings = (() *) \ ;
set D = [:(),((() *) \ ):];
reconsider ii = U -InterpretersOf S as Subset of () by XBOOLE_0:def 10;
reconsider subboolean = BOOLEAN as Subset of BOOLEAN by XBOOLE_0:def 10;
reconsider sub = [:ii,():] as Subset of [:(),((() *) \ ):] ;
[:sub,subboolean:] c= [:[:(),((() *) \ ):],BOOLEAN:] ;
then S -TruthEval U is PartFunc of [:(),((() *) \ ):],BOOLEAN by XBOOLE_1:1;
then reconsider Z = S -TruthEval U as Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) by PARTFUN1:45;
deffunc H1( Element of PFuncs ([:(),((() *) \ ):],BOOLEAN)) -> Element of bool [:[:(),((() *) \ ):],BOOLEAN:] = (() +* ()) +* \$1;
defpred S1[ set , Element of PFuncs ([:(),((() *) \ ):],BOOLEAN), set ] means \$3 = H1(\$2);
A1: for n being Nat
for x being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) ex y being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) ex y being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) st S1[n,x,y]
let x be Element of PFuncs ([:(),((() *) \ ):],BOOLEAN); :: thesis: ex y being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) st S1[n,x,y]
reconsider yy = H1(x) as Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) by PARTFUN1:45;
take y = yy; :: thesis: S1[n,x,y]
thus S1[n,x,y] ; :: thesis: verum
end;
consider f being sequence of (PFuncs ([:(),((() *) \ ):],BOOLEAN)) such that
A2: ( f . 0 = Z & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) from 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 A2; :: 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 A2; :: thesis: verum