deffunc H₁( Element of NAT ) -> Element of REAL = In ((a to_power ((b * $1) + c)),REAL);
consider h being sequence of REAL such that
A1: for n being Element of NAT holds h . n = H₁(n) from FUNCT_2:sch 4();
take h ; :: thesis: for n being Element of NAT holds h . n = a to_power ((b * n) + c)
let n be Element of NAT ; :: thesis: h . n = a to_power ((b * n) + c)
thus h . n = In ((a to_power ((b * n) + c)),REAL) by A1
.= In ((a to_power ((b * n) + c)),REAL)
.= a to_power ((b * n) + c) ; :: thesis: verum