reconsider ss = s as Element of product the Object-Kind of S by PBOOLE:155;
consider f being Function of NAT,(product the Object-Kind of S) such that
A1: f . 0 = ss and
A2: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 12();
take f . k ; :: thesis: ex f being Function of NAT,(product the Object-Kind 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₁(i,f . i) by A2
.= Following (p,(f . i)) ; :: thesis: verum