let a, b be Real; :: thesis: ( a >= 0 & b > 0 implies a to_power b >= 0 )
assume A1: a >= 0 ; :: thesis: ( not b > 0 or a to_power b >= 0 )
assume b > 0 ; :: thesis: a to_power b >= 0
then ( a = 0 implies a to_power b >= 0 ) by POWER:def 2;
hence a to_power b >= 0 by A1, POWER:34; :: thesis: verum