let a, b, c be real number ; ( a > 0 & b > 0 implies (a * b) to_power c = (a to_power c) * (b to_power c) )
assume that
A1:
a > 0
and
A2:
b > 0
; (a * b) to_power c = (a to_power c) * (b to_power c)
A3:
a * b > 0
by A1, A2, XREAL_1:131;
A4:
(a * b) #R c = (a #R c) * (b #R c)
by A1, A2, PREPOWER:92;
A5:
(a * b) #R c = (a #R c) * (b to_power c)
by A2, A4, Def2;
A6:
(a * b) #R c = (a to_power c) * (b to_power c)
by A1, A5, Def2;
thus
(a * b) to_power c = (a to_power c) * (b to_power c)
by A3, A6, Def2; verum