per cases
( a >= 0 or a < 0 )
;

end;

suppose
a >= 0
; :: thesis: a to_power b is integer

then
a in NAT
by INT_1:3;

then reconsider aa = a as Nat ;

aa to_power b is Integer ;

hence a to_power b is integer ; :: thesis: verum

end;then reconsider aa = a as Nat ;

aa to_power b is Integer ;

hence a to_power b is integer ; :: thesis: verum