deffunc H₂( set , State of S) -> State of S = Following $2;
let s1, s2 be State of S; :: thesis: ( ex f being Function of NAT , product the Object-Kind of S st
( s1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . i) ) ) & ex f being Function of NAT , product the Object-Kind of S st
( s2 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . i) ) ) implies s1 = s2 )
given f1 being Function of NAT , product the Object-Kind of S such that A2: s1 = f1 . k and
A3: f1 . 0 = s and
A4: for i being Nat holds f1 . (i + 1) = H₂(i,f1 . i) ; :: thesis: ( for f being Function of NAT , product the Object-Kind of S holds
( not s2 = f . k or not f . 0 = s or ex i being Nat st not f . (i + 1) = Following (f . i) ) or s1 = s2 )
given f2 being Function of NAT , product the Object-Kind of S such that A5: s2 = f2 . k and
A6: f2 . 0 = s and
A7: for i being Nat holds f2 . (i + 1) = H₂(i,f2 . i) ; :: thesis: s1 = s2
f1 = f2 from NAT_1:sch 16(A3, A4, A6, A7);
hence s1 = s2 by A2, A5; :: thesis: verum