( a > 1 & b < 0 ) by TA1;
hence a to_power b is light by POWER:36; :: thesis: verum