deffunc H₁( Nat, Element of bool (X \/ (AllFormulasOf S))) -> Subset of ($2 \/ (AllFormulasOf S)) = (D,(num . $1)) AddFormulaTo $2;
let IT1, IT2 be sequence of (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
A3: IT1 . 0 = X and
A4: for m being Nat holds IT1 . (m + 1) = H₁(m,IT1 . m) and
A5: IT2 . 0 = X and
A6: for m being Nat holds IT2 . (m + 1) = H₁(m,IT2 . m) ; :: thesis: IT1 = IT2
A7: for m being Nat holds IT1 . (m + 1) = H₁(m,IT1 . m) by A4;
A8: for m being Nat holds IT2 . (m + 1) = H₁(m,IT2 . m) by A6;
A9: dom IT1 = NAT by FUNCT_2:def 1;
A10: dom IT2 = NAT by FUNCT_2:def 1;
thus IT1 = IT2 from NAT_1:sch 15(A9, A3, A7, A10, A5, A8); :: thesis: verum