let a, b, p be Real; :: thesis: ( 0 < p & 0 <= a & a < b implies a to_power p < b to_power p )
assume A1: ( 0 < p & 0 <= a & a < b ) ; :: thesis: a to_power p < b to_power p
now :: thesis: ( a = 0 implies a to_power p < b to_power p )
assume a = 0 ; :: thesis: a to_power p < b to_power p
then a to_power p = 0 by A1, POWER:def 2;
hence a to_power p < b to_power p by A1, POWER:34; :: thesis: verum
end;
hence a to_power p < b to_power p by A1, POWER:37; :: thesis: verum