deffunc H₁( Nat, Real) -> Element of REAL = In (($2 * (s . ($1 + 1))),REAL);
consider f being sequence of REAL such that
A1: ( f . 0 = s . 0 & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 12();
reconsider f = f as Real_Sequence ;
take f ; :: thesis: ( f . 0 = s . 0 & ( for n being Nat holds f . (n + 1) = (f . n) * (s . (n + 1)) ) )
thus f . 0 = s . 0 by A1; :: thesis: for n being Nat holds f . (n + 1) = (f . n) * (s . (n + 1))
let n be Nat; :: thesis: f . (n + 1) = (f . n) * (s . (n + 1))
f . (n + 1) = H₁(n,f . n) by A1;
hence f . (n + 1) = (f . n) * (s . (n + 1)) ; :: thesis: verum