deffunc H₁( set , Subset of (HFuncs NAT)) -> Element of K32((HFuncs NAT)) = (PR-closure $2) \/ (composition-closure $2);
let it1, it2 be sequence of (bool (HFuncs NAT)); :: thesis: ( it1 . 0 = initial-funcs & ( for m being Nat holds it1 . (m + 1) = (PR-closure (it1 . m)) \/ (composition-closure (it1 . m)) ) & it2 . 0 = initial-funcs & ( for m being Nat holds it2 . (m + 1) = (PR-closure (it2 . m)) \/ (composition-closure (it2 . m)) ) implies it1 = it2 )
assume that
A3: it1 . 0 = initial-funcs and
A4: for m being Nat holds it1 . (m + 1) = (PR-closure (it1 . m)) \/ (composition-closure (it1 . m)) and
A5: it2 . 0 = initial-funcs and
A6: for m being Nat holds it2 . (m + 1) = (PR-closure (it2 . m)) \/ (composition-closure (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: it2 . 0 = initial-funcs by A5;
A10: it1 . 0 = initial-funcs by A3;
thus it1 = it2 from NAT_1:sch 16(A10, A7, A9, A8); :: thesis: verum