let s1, s2 be State of S; :: thesis: ( ex f being sequence of (product (the_Values_of S)) st

( s1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) & ex f being sequence of (product (the_Values_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 sequence of (product (the_Values_of S)) such that A3: s1 = f1 . k and

A4: f1 . 0 = s and

A5: for i being Nat holds f1 . (i + 1) = Following (p,(f1 . i)) ; :: thesis: ( for f being sequence of (product (the_Values_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 sequence of (product (the_Values_of S)) such that A6: s2 = f2 . k and

A7: f2 . 0 = s and

A8: for i being Nat holds f2 . (i + 1) = Following (p,(f2 . i)) ; :: thesis: s1 = s2

reconsider s = s as Element of product (the_Values_of S) by CARD_3:107;

A9: f1 . 0 = s by A4;

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

A11: f2 . 0 = s by A7;

A12: for i being Nat holds f2 . (i + 1) = H_{1}(i,f2 . i)
by A8;

f1 = f2 from NAT_1:sch 16(A9, A10, A11, A12);

hence s1 = s2 by A3, A6; :: thesis: verum

( s1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) & ex f being sequence of (product (the_Values_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 sequence of (product (the_Values_of S)) such that A3: s1 = f1 . k and

A4: f1 . 0 = s and

A5: for i being Nat holds f1 . (i + 1) = Following (p,(f1 . i)) ; :: thesis: ( for f being sequence of (product (the_Values_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 sequence of (product (the_Values_of S)) such that A6: s2 = f2 . k and

A7: f2 . 0 = s and

A8: for i being Nat holds f2 . (i + 1) = Following (p,(f2 . i)) ; :: thesis: s1 = s2

reconsider s = s as Element of product (the_Values_of S) by CARD_3:107;

A9: f1 . 0 = s by A4;

A10: for i being Nat holds f1 . (i + 1) = H

A11: f2 . 0 = s by A7;

A12: for i being Nat holds f2 . (i + 1) = H

f1 = f2 from NAT_1:sch 16(A9, A10, A11, A12);

hence s1 = s2 by A3, A6; :: thesis: verum