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