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

let F1, F2 be sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):]; :: thesis: ( F1 . 0 = s & ( for i being Nat holds F1 . (i + 1) = Following (F1 . i) ) & F2 . 0 = s & ( for i being Nat holds F2 . (i + 1) = Following (F2 . i) ) implies F1 = F2 )

assume that

A2: F1 . 0 = s and

A3: for i being Nat holds F1 . (i + 1) = Following (F1 . i) and

A4: F2 . 0 = s and

A5: for i being Nat holds F2 . (i + 1) = Following (F2 . i) ; :: thesis: F1 = F2

A6: for i being Nat holds F1 . (i + 1) = H_{1}(i,F1 . i)
by A3;

A7: for i being Nat holds F2 . (i + 1) = H_{1}(i,F2 . i)
by A5;

A8: F2 . 0 = s by A4;

A9: F1 . 0 = s by A2;

thus F1 = F2 from NAT_1:sch 16(A9, A6, A8, A7); :: thesis: verum

let F1, F2 be sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):]; :: thesis: ( F1 . 0 = s & ( for i being Nat holds F1 . (i + 1) = Following (F1 . i) ) & F2 . 0 = s & ( for i being Nat holds F2 . (i + 1) = Following (F2 . i) ) implies F1 = F2 )

assume that

A2: F1 . 0 = s and

A3: for i being Nat holds F1 . (i + 1) = Following (F1 . i) and

A4: F2 . 0 = s and

A5: for i being Nat holds F2 . (i + 1) = Following (F2 . i) ; :: thesis: F1 = F2

A6: for i being Nat holds F1 . (i + 1) = H

A7: for i being Nat holds F2 . (i + 1) = H

A8: F2 . 0 = s by A4;

A9: F1 . 0 = s by A2;

thus F1 = F2 from NAT_1:sch 16(A9, A6, A8, A7); :: thesis: verum