ex f being sequence of (product (the_Values_of S)) st
( Comput (p,s,0) = f . 0 & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) by Def7;
hence Comput (p,s,0) = s ; :: thesis: verum