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