let x be set ; :: thesis: for m being Nat
for f being Function
for p being FinSequence st rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds
p . (i + 1) = f . (p . i) ) holds
p . (m + 1) = (iter (f,m)) . x
let m be Nat; :: thesis: for f being Function
for p being FinSequence st rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds
p . (i + 1) = f . (p . i) ) holds
p . (m + 1) = (iter (f,m)) . x
let f be Function; :: thesis: for p being FinSequence st rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds
p . (i + 1) = f . (p . i) ) holds
p . (m + 1) = (iter (f,m)) . x
let p be FinSequence; :: thesis: ( rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds
p . (i + 1) = f . (p . i) ) implies p . (m + 1) = (iter (f,m)) . x )
B4: dom plus = COMPLEX by FUNCT_2:def 1;
then reconsider Z = 0 as Element of dom plus by XCMPLX_0:def 2;
reconsider g = p * plus as Function ;
B2: for z being complex number holds g . z = p . (z + 1)

proof

let z be complex number ; :: thesis: g . z = p . (z + 1)
reconsider zz = z as Element of dom plus by B4, XCMPLX_0:def 2;
thus g . z = p . (plus . zz) by FUNCT_1:13
.= p . (z + 1) by DefPlus ; :: thesis: verum

end;

assume B10: ( rng f c= dom f & x in dom f ) ; :: thesis: ( not p . 1 = x or ex i being Nat st
( i >= 1 & i < m + 1 & not p . (i + 1) = f . (p . i) ) or p . (m + 1) = (iter (f,m)) . x )
assume p . 1 = x ; :: thesis: ( ex i being Nat st
( i >= 1 & i < m + 1 & not p . (i + 1) = f . (p . i) ) or p . (m + 1) = (iter (f,m)) . x )
then p . (0 + 1) = x ;
then B0: g . 0 = x by B2;
assume B3: for i being Nat st i >= 1 & i < m + 1 holds
p . (i + 1) = f . (p . i) ; :: thesis: p . (m + 1) = (iter (f,m)) . x

now

let j be Nat; :: thesis: ( j < m implies g . (j + 1) = f . (g . j) )
reconsider jz = j as complex number ;
assume j < m ; :: thesis: g . (j + 1) = f . (g . j)
then ( j + 1 >= 0 + 1 & j + 1 < m + 1 ) by XREAL_1:7, XREAL_1:8;
then p . ((j + 1) + 1) = f . (p . (j + 1)) by B3
.= f . (g . j) by B2 ;
hence g . (j + 1) = f . (g . j) by B2; :: thesis: verum

end;

then g . m = (iter (f,m)) . x by Lm35, B0, B10;
hence p . (m + 1) = (iter (f,m)) . x by B2; :: thesis: verum