let x1, y1 be Real; :: thesis: ( x1 >= 0 & y1 > 0 implies x1 to_power y1 >= 0 )
assume that
A1: x1 >= 0 and
A2: y1 > 0 ; :: thesis: x1 to_power y1 >= 0
( x1 > 0 or x1 = 0 ) by A1;
hence x1 to_power y1 >= 0 by A2, POWER:34, POWER:def 2; :: thesis: verum