deffunc H₁( Element of NAT ) -> Element of REAL = In ((($1 + a) !),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 = (n + a) !
let n be Element of NAT ; :: thesis: h . n = (n + a) !
h . n = H₁(n) by A1;
hence h . n = (n + a) ! ; :: thesis: verum