:: deftheorem Def2 defines to_power POWER:def 2 :
for a, b, b₃ being Real holds
( ( a > 0 implies ( b₃ = a to_power b iff b₃ = a #R b ) ) & ( a = 0 & b > 0 implies ( b₃ = a to_power b iff b₃ = 0 ) ) & ( b is Integer implies ( b₃ = a to_power b iff ex k being Integer st
( k = b & b₃ = a #Z k ) ) ) );