deffunc H_{1}( Nat, Element of REAL ) -> Element of REAL = In (((a . ($1 + 1)) / (b to_power (($1 + 1) !))),REAL);

deffunc H_{2}() -> Element of REAL = In (0,REAL);

consider f being sequence of REAL such that

A1: ( f . 0 = H_{2}() & ( for n being Nat holds f . (n + 1) = H_{1}(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_{1}(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

deffunc H

consider f being sequence of REAL such that

A1: ( f . 0 = H

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

.= (a . (k + 1)) / (b to_power ((k + 1) !)) ;

hence f . n = (a . n) / (b to_power (n !)) by A2; :: thesis: verum