theorem PowerIn01: :: FUZIMPL1:5

for a, b being Element of [.0,1.] st ( a > 0 or b > 0 ) holds
b to_power a in [.0,1.]