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 A1: ( 0 < p & 0 < q ) ; :: thesis: for a being Real st 0 <= a holds
(a to_power p) to_power q = a to_power (p * q)
let a be Real; :: thesis: ( 0 <= a implies (a to_power p) to_power q = a to_power (p * q) )
assume A2: 0 <= a ; :: thesis: (a to_power p) to_power q = a to_power (p * q)
A3: 0 < p * q by A1, XREAL_1:131;

now

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

case A4: 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 A1, POWER:def 2 ;
hence (a to_power p) to_power q = a to_power (p * q) by A3, A4, 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 A2, POWER:38; :: thesis: verum

end;

end;

end;

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