thus ex f being Function of NAT , product the Object-Kind of SCM+FSA st
( f . 0 = s & ( for i being Nat holds f . (i + 1) = H₁(i,f . i) ) ) from NAT_1:sch 12(); :: thesis: verum