let F1, F2 be Function of NAT ,[:the States 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 & ( for i being Nat holds F1 . (i + 1) = Following (F1 . i) ) ) and
A3: ( F2 . 0 = s & ( for i being Nat holds F2 . (i + 1) = Following (F2 . i) ) ) ; :: thesis: F1 = F2
deffunc H₁( set , All-State of T) -> All-State of T = Following $2;
A4: F1 . 0 = s by A2;
B4: for i being Nat holds F1 . (i + 1) = H₁(i,F1 . i) by A2;
A5: F2 . 0 = s by A3;
B5: for i being Nat holds F2 . (i + 1) = H₁(i,F2 . i) by A3;
thus F1 = F2 from NAT_1:sch 16(A4, B4, A5, B5); :: thesis: verum