let X be set ; for n being Nat
for f being PartFunc of X,X holds iter (f,n) is PartFunc of X,X
let n be Nat; for f being PartFunc of X,X holds iter (f,n) is PartFunc of X,X
let f be PartFunc of X,X; iter (f,n) is PartFunc of X,X
A1:
field f = (dom f) \/ (rng f)
;
rng (iter (f,n)) c= field f
by Th71;
then A2:
rng (iter (f,n)) c= X
by A1, XBOOLE_1:1;
dom (iter (f,n)) c= field f
by Th71;
then
dom (iter (f,n)) c= X
by A1, XBOOLE_1:1;
hence
iter (f,n) is PartFunc of X,X
by A2, RELSET_1:4; verum