deffunc H_{1}( 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_{1}(n,F . n) ) )
from NAT_1:sch 12();

hence ex b_{1} being sequence of (Funcs (X,X)) st

( b_{1} . 0 = id X & ( for i being Nat holds b_{1} . (i + 1) = f * (b_{1} . i) ) )
; :: thesis: verum

ex F being sequence of (Funcs (X,X)) st

( F . 0 = id X & ( for n being Nat holds F . (n + 1) = H

hence ex b

( b