let a be object ; :: thesis: for X being set
for f being Function
for n being Nat st n <> 0 & a in X & f = X --> a holds
iter (f,n) = f
let X be set ; :: thesis: for f being Function
for n being Nat st n <> 0 & a in X & f = X --> a holds
iter (f,n) = f
let f be Function; :: thesis: for n being Nat st n <> 0 & a in X & f = X --> a holds
iter (f,n) = f
let n be Nat; :: thesis: ( n <> 0 & a in X & f = X --> a implies iter (f,n) = f )
assume that
A1: n <> 0 and
A2: a in X and
A3: f = X --> a ; :: thesis: iter (f,n) = f
defpred S₁[ Nat] means iter (f,($1 + 1)) = f;

A4: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

A5: dom f = X by A3;
let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]

A7: now :: thesis: for x being object st x in dom f holds
(iter (f,((k + 1) + 1))) . x = f . x

let x be object ; :: thesis: ( x in dom f implies (iter (f,((k + 1) + 1))) . x = f . x )
assume A8: x in dom f ; :: thesis: (iter (f,((k + 1) + 1))) . x = f . x
then A9: f . x = a by A3, FUNCOP_1:7;
thus (iter (f,((k + 1) + 1))) . x = (f * f) . x by A6, Th70
.= f . (f . x) by A8, FUNCT_1:13
.= f . x by A2, A3, A9, FUNCOP_1:7 ; :: thesis: verum

end;

rng f = {a} by A2, A3, FUNCOP_1:8;
then rng f c= dom f by A2, A5, ZFMISC_1:31;
then dom (iter (f,((k + 1) + 1))) = dom f by Th73;
hence S₁[k + 1] by A7, FUNCT_1:2; :: thesis: verum

end;

A10: S₁[ 0 ] by Th69;
A11: for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A4);
consider k being Nat such that
A12: n = k + 1 by A1, NAT_1:6;
reconsider k = k as Nat ;
n = k + 1 by A12;
hence iter (f,n) = f by A11; :: thesis: verum