let f, g be Function; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ((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; :: thesis: verum