deffunc H₁( set , Subset of (HFuncs NAT)) -> Element of K32((HFuncs NAT)) = (PR-closure $2) \/ (composition-closure $2);
consider A being sequence of (bool (HFuncs NAT)) such that
A1: A . 0 = initial-funcs and
A2: for m being Nat holds A . (m + 1) = H₁(m,A . m) from NAT_1:sch 12();
take A ; :: thesis: ( A . 0 = initial-funcs & ( for m being Nat holds A . (m + 1) = (PR-closure (A . m)) \/ (composition-closure (A . m)) ) )
thus A . 0 = initial-funcs by A1; :: thesis: for m being Nat holds A . (m + 1) = (PR-closure (A . m)) \/ (composition-closure (A . m))
let m be Nat; :: thesis: A . (m + 1) = (PR-closure (A . m)) \/ (composition-closure (A . m))
thus A . (m + 1) = (PR-closure (A . m)) \/ (composition-closure (A . m)) by A2; :: thesis: verum