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

consider f being sequence of (product (the_Values_of S)) such that

A1: f . 0 = ss and

A2: for n being Nat holds f . (n + 1) = H_{1}(n,f . n)
from NAT_1:sch 12();

take f . k ; :: thesis: ex f being sequence of (product (the_Values_of S)) st

( f . k = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )

take f ; :: thesis: ( f . k = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )

thus f . k = f . k ; :: thesis: ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )

thus f . 0 = s by A1; :: thesis: for i being Nat holds f . (i + 1) = Following (p,(f . i))

let i be Nat; :: thesis: f . (i + 1) = Following (p,(f . i))

thus f . (i + 1) = H_{1}(i,f . i)
by A2

.= Following (p,(f . i)) ; :: thesis: verum

consider f being sequence of (product (the_Values_of S)) such that

A1: f . 0 = ss and

A2: for n being Nat holds f . (n + 1) = H

take f . k ; :: thesis: ex f being sequence of (product (the_Values_of S)) st

( f . k = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )

take f ; :: thesis: ( f . k = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )

thus f . k = f . k ; :: thesis: ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )

thus f . 0 = s by A1; :: thesis: for i being Nat holds f . (i + 1) = Following (p,(f . i))

let i be Nat; :: thesis: f . (i + 1) = Following (p,(f . i))

thus f . (i + 1) = H

.= Following (p,(f . i)) ; :: thesis: verum