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