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