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: S₁[ 0 ] by Th72;

A5: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
A7: ( dom f = X & rng f = {a} ) by A2, A3, FUNCOP_1:14, FUNCOP_1:19;
then rng f c= dom f by A2, ZFMISC_1:37;
then A8: dom (iter f,((k + 1) + 1)) = dom f by Th76;

now

let x be set ; :: thesis: ( x in dom f implies (iter f,((k + 1) + 1)) . x = f . x )
assume A9: x in dom f ; :: thesis: (iter f,((k + 1) + 1)) . x = f . x
then A10: f . x = a by A3, A7, FUNCOP_1:13;
thus (iter f,((k + 1) + 1)) . x = (f * f) . x by A6, Th73
.= f . (f . x) by A9, FUNCT_1:23
.= f . x by A2, A3, A10, FUNCOP_1:13 ; :: thesis: verum

end;

hence S₁[k + 1] by A8, FUNCT_1:9; :: thesis: verum

end;

A11: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
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