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 that
A1: 0 < p and
A2: 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 A3: 0 <= a ; :: thesis: (a to_power p) * (a to_power q) = a to_power (p + q)

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

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 A1, A2, 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 A3, POWER:27; :: thesis: verum

end;

end;

end;

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