let n be Nat; :: thesis: for a being Real st 1 <= a holds
a to_power n <= a to_power (n + 1)
let a be Real; :: thesis: ( 1 <= a implies a to_power n <= a to_power (n + 1) )
assume AS: 1 <= a ; :: thesis: a to_power n <= a to_power (n + 1)
LP3: a to_power (n + 1) = (a to_power n) * (a to_power 1) by FIB_NUM2:5
.= (a to_power n) * a by POWER:25 ;
a to_power n > 0 by POWER:34, AS;
then 1 * (a to_power n) <= (a to_power n) * a by XREAL_1:64, AS;
hence a to_power n <= a to_power (n + 1) by LP3; :: thesis: verum