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 ) ;
end;
end;
hence (a to_power p) to_power q = a to_power (p * q) ; :: thesis: verum