consider f being Function of NAT ,(product the Object-Kind of S) such that
W1: f . 0 = s and
W2: 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 & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) ) by W1, W2; :: thesis: verum