let p, q be Real; :: thesis: ( 0 < p & 0 < q implies for a being Real st 0 <= a holds
(a to_power p) to_power q = a to_power (p * q) )
assume that
A1: 0 < p and
A2: 0 < q ; :: thesis: for a being Real st 0 <= a holds
(a to_power p) to_power q = a to_power (p * q)
A3: 0 < p * q by A1, A2, XREAL_1:129;
let a be Real; :: thesis: ( 0 <= a implies (a to_power p) to_power q = a to_power (p * q) )
assume A4: 0 <= a ; :: thesis: (a to_power p) to_power q = a to_power (p * q)

now :: thesis: ( ( a = 0 & (a to_power p) to_power q = a to_power (p * q) ) or ( a <> 0 & (a to_power p) to_power q = a to_power (p * q) ) )

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

case A5: a = 0 ; :: thesis: (a to_power p) to_power q = a to_power (p * q)

then (a to_power p) to_power q = 0 to_power q by A1, POWER:def 2
.= 0 by A2, POWER:def 2 ;
hence (a to_power p) to_power q = a to_power (p * q) by A3, A5, POWER:def 2; :: thesis: verum

end;

case a <> 0 ; :: thesis: (a to_power p) to_power q = a to_power (p * q)

hence (a to_power p) to_power q = a to_power (p * q) by A4, POWER:33; :: thesis: verum

end;

end;

end;

hence (a to_power p) to_power q = a to_power (p * q) ; :: thesis: verum