deffunc H₁( Nat, Element of Funcs (X,X)) -> Element of Funcs (X,X) = f * $2;
ex F being sequence of (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 sequence of (Funcs (X,X)) st
( b₁ . 0 = id X & ( for i being Nat holds b₁ . (i + 1) = f * (b₁ . i) ) ) ; :: thesis: verum