let a, X be set ; :: thesis: for f being Function
for n being Element of NAT st n <> 0 & a in X & f = X --> a holds
iter f,n = f
let f be Function; :: thesis: for n being Element of NAT st n <> 0 & a in X & f = X --> a holds
iter f,n = f
let n be Element of 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₁[ Element of NAT ] means iter f,($1 + 1) = f;

A4: now

A5: dom f = X by A3, FUNCOP_1:19;
let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]

A7: now

let x be set ; :: 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, A5, FUNCOP_1:13;
thus (iter f,((k + 1) + 1)) . x = (f * f) . x by A6, Th73
.= f . (f . x) by A8, FUNCT_1:23
.= f . x by A2, A3, A9, FUNCOP_1:13 ; :: thesis: verum

end;

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

end;

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