set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set AF = AtomicFormulasOf S;
set Strings = (() *) \ ;
set D = [:(),((() *) \ ):];
set Z = S -TruthEval U;
( [:(),():] c= [:(),((() *) \ ):] & BOOLEAN c= BOOLEAN ) by ZFMISC_1:96;
then ( dom () c= [:(),((() *) \ ):] & rng () c= BOOLEAN ) ;
then S -TruthEval U is Relation of [:(),((() *) \ ):],BOOLEAN by RELSET_1:4;
then reconsider ZZ = S -TruthEval U as Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) by PARTFUN1:45;
deffunc H1( set , Element of PFuncs ([:(),((() *) \ ):],BOOLEAN)) -> Element of bool [:[:(),((() *) \ ):],BOOLEAN:] = (() +* ()) +* \$2;
defpred S1[ set , set , set ] means for f being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) st \$2 = f holds
\$3 = H1(\$1,f);
let IT1, IT2 be sequence of (PFuncs ([:(),((() *) \ ):],BOOLEAN)); :: thesis: ( IT1 . 0 = S -TruthEval U & ( for mm being Element of NAT holds IT1 . (mm + 1) = ((ExIterator (IT1 . mm)) +* (NorIterator (IT1 . mm))) +* (IT1 . mm) ) & IT2 . 0 = S -TruthEval U & ( for mm being Element of NAT holds IT2 . (mm + 1) = ((ExIterator (IT2 . mm)) +* (NorIterator (IT2 . mm))) +* (IT2 . mm) ) implies IT1 = IT2 )
assume A3: ( IT1 . 0 = S -TruthEval U & ( for mm being Element of NAT holds IT1 . (mm + 1) = ((ExIterator (IT1 . mm)) +* (NorIterator (IT1 . mm))) +* (IT1 . mm) ) ) ; :: thesis: ( not IT2 . 0 = S -TruthEval U or ex mm being Element of NAT st not IT2 . (mm + 1) = ((ExIterator (IT2 . mm)) +* (NorIterator (IT2 . mm))) +* (IT2 . mm) or IT1 = IT2 )
assume A4: ( IT2 . 0 = S -TruthEval U & ( for mm being Element of NAT holds IT2 . (mm + 1) = ((ExIterator (IT2 . mm)) +* (NorIterator (IT2 . mm))) +* (IT2 . mm) ) ) ; :: thesis: IT1 = IT2
A5: IT1 . 0 = ZZ by A3;
A6: for m being Nat holds S1[m,IT1 . m,IT1 . (m + 1)]
proof
let m be Nat; :: thesis: S1[m,IT1 . m,IT1 . (m + 1)]
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
let f be Element of PFuncs ([:(),((() *) \ ):],BOOLEAN); :: thesis: ( IT1 . m = f implies IT1 . (m + 1) = H1(m,f) )
assume f = IT1 . m ; :: thesis: IT1 . (m + 1) = H1(m,f)
then IT1 . (mm + 1) = H1(m,f) by A3;
hence IT1 . (m + 1) = H1(m,f) ; :: thesis: verum
end;
A7: IT2 . 0 = ZZ by A4;
A8: for m being Nat holds S1[m,IT2 . m,IT2 . (m + 1)]
proof
let m be Nat; :: thesis: S1[m,IT2 . m,IT2 . (m + 1)]
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
let f be Element of PFuncs ([:(),((() *) \ ):],BOOLEAN); :: thesis: ( IT2 . m = f implies IT2 . (m + 1) = H1(m,f) )
assume f = IT2 . m ; :: thesis: IT2 . (m + 1) = H1(m,f)
then IT2 . (mm + 1) = H1(m,f) by A4;
hence IT2 . (m + 1) = H1(m,f) ; :: thesis: verum
end;
A9: for n being Nat
for x, y1, y2 being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
proof
let n be Nat; :: thesis: for x, y1, y2 being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN) st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2

let x, y1, y2 be Element of PFuncs ([:(),((() *) \ ):],BOOLEAN); :: thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 )
assume that
A10: S1[n,x,y1] and
A11: S1[n,x,y2] ; :: thesis: y1 = y2
A12: y2 = H1(n,x) by A11;
thus y1 = y2 by ; :: thesis: verum
end;
thus IT1 = IT2 from NAT_1:sch 14(A5, A6, A7, A8, A9); :: thesis: verum