deffunc H₁( Nat, Element of bool (X \/ (AllFormulasOf S))) -> Subset of ($2 \/ (AllFormulasOf S)) = (D,(num . $1)) AddAsWitnessTo $2;
let IT1, IT2 be Function of NAT,(bool (X \/ (AllFormulasOf S))); :: thesis: ( IT1 . 0 = X & ( for mm being Element of NAT holds IT1 . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (IT1 . mm) ) & IT2 . 0 = X & ( for mm being Element of NAT holds IT2 . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (IT2 . mm) ) implies IT1 = IT2 )
assume that
B2: IT1 . 0 = X and
B13: for mm being Element of NAT holds IT1 . (mm + 1) = H₁(mm,IT1 . mm) and
B5: IT2 . 0 = X and
B16: for mm being Element of NAT holds IT2 . (mm + 1) = H₁(mm,IT2 . mm) ; :: thesis: IT1 = IT2
B3: for m being Nat holds IT1 . (m + 1) = H₁(m,IT1 . m)

proof

let m be Nat; :: thesis: IT1 . (m + 1) = H₁(m,IT1 . m)
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
IT1 . (mm + 1) = H₁(mm,IT1 . mm) by B13;
hence IT1 . (m + 1) = H₁(m,IT1 . m) ; :: thesis: verum

end;

B6: for m being Nat holds IT2 . (m + 1) = H₁(m,IT2 . m)

proof

let m be Nat; :: thesis: IT2 . (m + 1) = H₁(m,IT2 . m)
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
IT2 . (mm + 1) = H₁(mm,IT2 . mm) by B16;
hence IT2 . (m + 1) = H₁(m,IT2 . m) ; :: thesis: verum

end;

B1: dom IT1 = NAT by FUNCT_2:def 1;
B4: dom IT2 = NAT by FUNCT_2:def 1;
thus IT1 = IT2 from NAT_1:sch 15(B1, B2, B3, B4, B5, B6); :: thesis: verum