let a, b, c be Real; :: thesis: ( a >= 0 & b >= 0 & c > 0 implies (a * b) to_power c = (a to_power c) * (b to_power c) )
assume that
A1: ( a >= 0 & b >= 0 ) and
A2: c > 0 ; :: thesis: (a * b) to_power c = (a to_power c) * (b to_power c)

now :: thesis: ( ( a = 0 or b = 0 ) implies (a * b) to_power c = (a to_power c) * (b to_power c) )

assume A3: ( a = 0 or b = 0 ) ; :: thesis: (a * b) to_power c = (a to_power c) * (b to_power c)
then (a * b) to_power c = 0 by A2, POWER:def 2;
hence (a * b) to_power c = (a to_power c) * (b to_power c) by A3; :: thesis: verum

end;

hence (a * b) to_power c = (a to_power c) * (b to_power c) by A1, POWER:30; :: thesis: verum