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