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
(dom f) \/ (rng f) = dom f by A1, XBOOLE_1:12;
then iter f,0 = id (dom f) by FUNCT_7:70;
then A4: a = (iter f,0 ) . a by A2, 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, A3, A4, Def7; :: thesis: verum