deffunc H_{1}( set , All-State of T) -> All-State of T = Following $2;

consider f being sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] such that

A1: ( f . 0 = s & ( for n being Nat holds f . (n + 1) = H_{1}(n,f . n) ) )
from NAT_1:sch 12();

take f ; :: thesis: ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . i) ) )

thus ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . i) ) ) by A1; :: thesis: verum

consider f being sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] such that

A1: ( f . 0 = s & ( for n being Nat holds f . (n + 1) = H

take f ; :: thesis: ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . i) ) )

thus ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . i) ) ) by A1; :: thesis: verum