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 A1: ( rng f c= dom f & a in dom f & a nin A ) ; :: thesis: (A,g iter f) . a = a
then (dom f) \/ (rng f) = dom f by XBOOLE_1:12;
then iter f,0 = id (dom f) by FUNCT_7:70;
then A2: a = (iter f,0 ) . a by A1, FUNCT_1:35;
for i being Nat st i < 0 holds
(iter f,i) . a in A ;
hence (A,g iter f) . a = a by A1, A2, Def7; :: thesis: verum