deffunc H₁( Nat, Element of REAL ) -> Element of REAL = $2 * ($1 + 1);
consider f being Function of NAT,REAL such that
A1: ( f . 0 = 1 & ( 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 Element of NAT holds f . (n + 1) = (f . n) * (n + 1) ) )
thus ( f . 0 = 1 & ( for n being Element of NAT holds f . (n + 1) = (f . n) * (n + 1) ) ) by A1; :: thesis: verum