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