reconsider m = n - 1 as Nat ;
( a |^ (m + 1) = a * (a |^ m) & a > 1 ) by NEWTON:6, Def0;
then ( a |^ (m + 1) > 1 * (a |^ m) & a |^ m >= 1 ) by XREAL_1:68, NAT_1:14;
hence not a |^ n is trivial by XXREAL_0:2; :: thesis: verum