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 (p,(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 (p,(f . i)) ) ) implies s1 = s2 )
given f1 being Function of NAT,(product the Object-Kind of S) such that A3: s1 = f1 . k and
B4: f1 . 0 = s and
B5: for i being Nat holds f1 . (i + 1) = Following (p,(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 (p,(f . i)) ) or s1 = s2 )
given f2 being Function of NAT,(product the Object-Kind of S) such that A6: s2 = f2 . k and
B7: f2 . 0 = s and
B8: for i being Nat holds f2 . (i + 1) = Following (p,(f2 . i)) ; :: thesis: s1 = s2
reconsider s = s as Element of product the Object-Kind of S by PBOOLE:155;
A4: f1 . 0 = s by B4;
A5: for i being Nat holds f1 . (i + 1) = H₁(i,f1 . i) by B5;
A7: f2 . 0 = s by B7;
A8: for i being Nat holds f2 . (i + 1) = H₁(i,f2 . i) by B8;
f1 = f2 from NAT_1:sch 16(A4, A5, A7, A8);
hence s1 = s2 by A3, A6; :: thesis: verum