theorem :: FUNCT_7:80

for n being Nat holds iter ({},n) = {}