deffunc H₁( Nat, Element of Funcs X,X) -> Element of Funcs X,X = f * $2;
ex F being Function of NAT ,(Funcs X,X) st
( F . 0 = id X & ( for n being Nat holds F . (n + 1) = H₁(n,F . n) ) ) from NAT_1:sch 12();
hence ex b₁ being Function of NAT ,(Funcs X,X) st
( b₁ . 0 = id X & ( for i being Nat holds b₁ . (i + 1) = f * (b₁ . i) ) ) ; :: thesis: verum