reconsider z9 = z as Element of COMPLEX by XCMPLX_0:def 2;
deffunc H₁( set , Element of COMPLEX ) -> Element of COMPLEX = In (($2 * z9),COMPLEX);
consider f being sequence of COMPLEX such that
A1: ( f . 0 = 1r & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 12();
take f ; :: thesis: ( f . 0 = 1r & ( for n being Nat holds f . (n + 1) = (f . n) * z ) )
thus f . 0 = 1r by A1; :: thesis: for n being Nat holds f . (n + 1) = (f . n) * z
let n be Nat; :: thesis: f . (n + 1) = (f . n) * z
f . (n + 1) = H₁(n,f . n) by A1;
hence f . (n + 1) = (f . n) * z ; :: thesis: verum