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