let x be set ; :: thesis: for m being Nat
for g, f being Function st rng f c= dom f & x in dom f & g . 0 = x & ( for i being Nat st i < m holds
g . (i + 1) = f . (g . i) ) holds
g . m = (iter (f,m)) . x
let m be Nat; :: thesis: for g, f being Function st rng f c= dom f & x in dom f & g . 0 = x & ( for i being Nat st i < m holds
g . (i + 1) = f . (g . i) ) holds
g . m = (iter (f,m)) . x
let g, f be Function; :: thesis: ( rng f c= dom f & x in dom f & g . 0 = x & ( for i being Nat st i < m holds
g . (i + 1) = f . (g . i) ) implies g . m = (iter (f,m)) . x )
assume B10: ( rng f c= dom f & x in dom f ) ; :: thesis: ( not g . 0 = x or ex i being Nat st
( i < m & not g . (i + 1) = f . (g . i) ) or g . m = (iter (f,m)) . x )
then B11: x in (dom f) \/ (rng f) by XBOOLE_0:def 3;
defpred S₁[ Nat] means ( g . 0 = x & ( for i being Nat st i < $1 holds
g . (i + 1) = f . (g . i) ) implies g . $1 = (iter (f,$1)) . x );
B0: S₁[ 0 ]

proof

Z1: iter (f,0) = id (field f) by FUNCT_7:68;
assume ( g . 0 = x & ( for i being Nat st i < 0 holds
g . (i + 1) = f . (g . i) ) ) ; :: thesis: g . 0 = (iter (f,0)) . x
hence g . 0 = (iter (f,0)) . x by Z1, B11, FUNCT_1:17; :: thesis: verum

end;

B1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume C0: S₁[n] ; :: thesis: S₁[n + 1]
assume C1: g . 0 = x ; :: thesis: ( ex i being Nat st
( i < n + 1 & not g . (i + 1) = f . (g . i) ) or g . (n + 1) = (iter (f,(n + 1))) . x )
assume C2: for i being Nat st i < n + 1 holds
g . (i + 1) = f . (g . i) ; :: thesis: g . (n + 1) = (iter (f,(n + 1))) . x
Z3: for i being Nat st i < n holds
g . (i + 1) = f . (g . i)

proof

let i be Nat; :: thesis: ( i < n implies g . (i + 1) = f . (g . i) )
assume i < n ; :: thesis: g . (i + 1) = f . (g . i)
then i + 0 < n + 1 by XREAL_1:8;
hence g . (i + 1) = f . (g . i) by C2; :: thesis: verum

end;

C4: x in dom (iter (f,n)) by B10, FUNCT_7:74;
n + 0 < n + 1 by XREAL_1:8;
then g . (n + 1) = f . (g . n) by C2
.= (f * (iter (f,n))) . x by C4, Z3, C0, C1, FUNCT_1:13
.= (iter (f,(n + 1))) . x by FUNCT_7:71 ;
hence g . (n + 1) = (iter (f,(n + 1))) . x ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(B0, B1);
hence ( not g . 0 = x or ex i being Nat st
( i < m & not g . (i + 1) = f . (g . i) ) or g . m = (iter (f,m)) . x ) ; :: thesis: verum