reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
iter (f,n9) is Function of S,S ;
hence f |** n is Function of S,S ; :: thesis: verum