set SS = AllSymbolsOf S;
set II = U -InterpretersOf S;
set AF = AtomicFormulasOf S;
set Strings = ((AllSymbolsOf S) *) \ {{}};
set D = [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):];
set Z = S -TruthEval U;
( [:(U -InterpretersOf S),(AtomicFormulasOf S):] c= [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] & BOOLEAN c= BOOLEAN ) by ZFMISC_1:96;
then ( dom (S -TruthEval U) c= [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] & rng (S -TruthEval U) c= BOOLEAN ) by XBOOLE_1:1;
then S -TruthEval U is Relation of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN by RELSET_1:4;
then reconsider ZZ = S -TruthEval U as Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) by PARTFUN1:45;
deffunc H₁( set , Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) -> Element of bool [:[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN:] = ((ExIterator $2) +* (NorIterator $2)) +* $2;
defpred S₁[ set , set , set ] means for f being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st $2 = f holds
$3 = H₁($1,f);
let IT1, IT2 be Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],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 B11: ( 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 B12: ( 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
B1: IT1 . 0 = ZZ by B11;
B2: for m being Nat holds S₁[m,IT1 . m,IT1 . (m + 1)]

proof

let m be Nat; :: thesis: S₁[m,IT1 . m,IT1 . (m + 1)]
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
let f be Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN); :: thesis: ( IT1 . m = f implies IT1 . (m + 1) = H₁(m,f) )
assume f = IT1 . m ; :: thesis: IT1 . (m + 1) = H₁(m,f)
then IT1 . (mm + 1) = H₁(m,f) by B11;
hence IT1 . (m + 1) = H₁(m,f) ; :: thesis: verum

end;

B3: IT2 . 0 = ZZ by B12;
B4: for m being Nat holds S₁[m,IT2 . m,IT2 . (m + 1)]

proof

let m be Nat; :: thesis: S₁[m,IT2 . m,IT2 . (m + 1)]
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
let f be Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN); :: thesis: ( IT2 . m = f implies IT2 . (m + 1) = H₁(m,f) )
assume f = IT2 . m ; :: thesis: IT2 . (m + 1) = H₁(m,f)
then IT2 . (mm + 1) = H₁(m,f) by B12;
hence IT2 . (m + 1) = H₁(m,f) ; :: thesis: verum

end;

B5: for n being Nat
for x, y1, y2 being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2

proof

let n be Nat; :: thesis: for x, y1, y2 being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2
let x, y1, y2 be Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN); :: thesis: ( S₁[n,x,y1] & S₁[n,x,y2] implies y1 = y2 )
assume that
C1: S₁[n,x,y1] and
C2: S₁[n,x,y2] ; :: thesis: y1 = y2
C4: y2 = H₁(n,x) by C2;
thus y1 = y2 by C1, C4; :: thesis: verum

end;

thus IT1 = IT2 from NAT_1:sch 14(B1, B2, B3, B4, B5); :: thesis: verum