reconsider n = n as Element of NAT by ORDINAL1:def 13;
(power R) . a,n is Element of R ;
hence (power R) . a,n is Element of R ; :: thesis: verum