( (1 / a) to_power (- b) is light & (1 / a) to_power (- b) is positive ) ;
then a to_power (- (- b)) is light by POWER:32;
hence a to_power b is light ; :: thesis: verum