deffunc H1( Nat, Element of bool (X \/ (AllFormulasOf S))) -> Subset of ($2 \/ (AllFormulasOf S)) = (D,(num . $1)) AddAsWitnessTo $2;
let IT1, IT2 be sequence of (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
A3: IT1 . 0 = X and
A4: for mm being Element of NAT holds IT1 . (mm + 1) = H1(mm,IT1 . mm) and
A5: IT2 . 0 = X and
A6: for mm being Element of NAT holds IT2 . (mm + 1) = H1(mm,IT2 . mm) ; :: thesis: IT1 = IT2
A7: for m being Nat holds IT1 . (m + 1) = H1(m,IT1 . m)
proof
let m be Nat; :: thesis: IT1 . (m + 1) = H1(m,IT1 . m)
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
IT1 . (mm + 1) = H1(mm,IT1 . mm) by A4;
hence IT1 . (m + 1) = H1(m,IT1 . m) ; :: thesis: verum
end;
A8: for m being Nat holds IT2 . (m + 1) = H1(m,IT2 . m)
proof
let m be Nat; :: thesis: IT2 . (m + 1) = H1(m,IT2 . m)
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
IT2 . (mm + 1) = H1(mm,IT2 . mm) by A6;
hence IT2 . (m + 1) = H1(m,IT2 . m) ; :: thesis: verum
end;
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