let f, g be Function; for a, A being set st rng f c= dom f & a in dom f & a nin A holds
((A,g) iter f) . a = a
let a, A be set ; ( rng f c= dom f & a in dom f & a nin A implies ((A,g) iter f) . a = a )
assume that
A1:
rng f c= dom f
and
A2:
a in dom f
and
A3:
a nin A
; ((A,g) iter f) . a = a
field f = dom f
by A1, XBOOLE_1:12;
then
iter (f,0) = id (dom f)
by FUNCT_7:68;
then A4:
a = (iter (f,0)) . a
by A2, FUNCT_1:18;
for i being Nat st i < 0 holds
(iter (f,i)) . a in A
;
hence
((A,g) iter f) . a = a
by A1, A2, A3, A4, Def7; verum