deffunc H₁( Nat, Element of REAL ) -> Element of REAL = In (((a . ($1 + 1)) / (b to_power (($1 + 1) !))),REAL);
deffunc H₂() -> Element of REAL = In (0,REAL);
consider f being sequence of REAL such that
A1: ( f . 0 = H₂() & ( 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 = 0 & ( for k being non zero Nat holds f . k = (a . k) / (b to_power (k !)) ) )
thus f . 0 = 0 by A1; :: thesis: for k being non zero Nat holds f . k = (a . k) / (b to_power (k !))
let n be non zero Nat; :: thesis: f . n = (a . n) / (b to_power (n !))
consider k being Nat such that
A2: k + 1 = n by NAT_1:6;
f . (k + 1) = H₁(k,f . k) by A1
.= (a . (k + 1)) / (b to_power ((k + 1) !)) ;
hence f . n = (a . n) / (b to_power (n !)) by A2; :: thesis: verum