let x be set ; :: thesis: for p being FinSequence
for m being Nat
for f being Function 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: for m being Nat
for f being Function 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 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: ( 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 )
A1: 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 ;
A2: for z being Complex holds g . z = p . (z + 1)

proof

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

end;

assume A3: ( 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 A4: g . 0 = x by A2;
assume A5: 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 :: thesis: for j being Nat st j < m holds
g . (j + 1) = f . (g . j)

let j be Nat; :: thesis: ( j < m implies g . (j + 1) = f . (g . j) )
reconsider jz = j as Complex ;
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 A5
.= f . (g . j) by A2 ;
hence g . (j + 1) = f . (g . j) by A2; :: thesis: verum

end;

then g . m = (iter (f,m)) . x by Lm34, A4, A3;
hence p . (m + 1) = (iter (f,m)) . x by A2; :: thesis: verum