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

now

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

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

then (a to_power p) * (a to_power q) = 0 * (0 to_power q) by A1, POWER:def 2
.= 0 ;
hence (a to_power p) * (a 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) * (a to_power q) = a to_power (p + q)

hence (a to_power p) * (a to_power q) = a to_power (p + q) by A2, POWER:32; :: thesis: verum

end;

end;

end;

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