let x, p be real number ; :: thesis: ( x > 0 implies ( #R p is_differentiable_in x & diff (#R p),x = p * (x #R (p - 1)) ) )
set f = #R p;
A1: p is Real by XREAL_0:def 1;
A2: for x being Real st 0 < x holds
( exp_R * (p (#) ln ) is_differentiable_in x & diff (exp_R * (p (#) ln )),x = p * (x #R (p - 1)) )

proof

let x be Real; :: thesis: ( 0 < x implies ( exp_R * (p (#) ln ) is_differentiable_in x & diff (exp_R * (p (#) ln )),x = p * (x #R (p - 1)) ) )
assume A3: x > 0 ; :: thesis: ( exp_R * (p (#) ln ) is_differentiable_in x & diff (exp_R * (p (#) ln )),x = p * (x #R (p - 1)) )
A4: ln is_differentiable_in x by A3, Th18;
then A5: p (#) ln is_differentiable_in x by A1, FDIFF_1:23;
x in { g where g is Real : 0 < g } by A3;
then A6: x in right_open_halfline 0 by XXREAL_1:230;
then A7: x in dom (p (#) ln ) by Th18, VALUED_1:def 5;
A8: diff (p (#) ln ),x = p * (diff ln ,x) by A1, A4, FDIFF_1:23
.= p * (1 / x) by A6, Th18 ;
A9: exp_R is_differentiable_in (p (#) ln ) . x by SIN_COS:70;
hence exp_R * (p (#) ln ) is_differentiable_in x by A5, FDIFF_2:13; :: thesis: diff (exp_R * (p (#) ln )),x = p * (x #R (p - 1))
diff exp_R ,((p (#) ln ) . x) = exp_R . ((p (#) ln ) . x) by Th16
.= exp_R . (p * (ln . x)) by A7, VALUED_1:def 5
.= exp_R . (p * (log number_e ,x)) by A6, Def2
.= exp_R . (log number_e ,(x to_power p)) by A3, Lm4, POWER:63
.= x to_power p by A3, Th15, POWER:39 ;
hence diff (exp_R * (p (#) ln )),x = (x to_power p) * (p * (1 / x)) by A5, A9, A8, FDIFF_2:13
.= p * ((x to_power p) * (1 / x))
.= p * ((x to_power p) * (1 / (x to_power 1))) by POWER:30
.= p * ((x to_power p) * (x to_power (- 1))) by A3, POWER:33
.= p * (x to_power (p + (- 1))) by A3, POWER:32
.= p * (x #R (p - 1)) by A3, POWER:def 2 ;
:: thesis: verum

end;

rng (p (#) ln ) c= dom exp_R by Th16;
then A10: dom (exp_R * (p (#) ln )) = dom (p (#) ln ) by RELAT_1:46
.= right_open_halfline 0 by Th18, VALUED_1:def 5 ;
A11: for d being Element of REAL st d in right_open_halfline 0 holds
(exp_R * (p (#) ln )) . d = (#R p) . d

proof

let d be Element of REAL ; :: thesis: ( d in right_open_halfline 0 implies (exp_R * (p (#) ln )) . d = (#R p) . d )
assume A12: d in right_open_halfline 0 ; :: thesis: (exp_R * (p (#) ln )) . d = (#R p) . d
A13: d in dom (p (#) ln ) by A12, Th18, VALUED_1:def 5;
d in { g where g is Real : 0 < g } by A12, XXREAL_1:230;
then A14: ex g being Real st
( g = d & g > 0 ) ;
thus (exp_R * (p (#) ln )) . d = (exp_R * (p (#) ln )) /. d by A10, A12, PARTFUN1:def 8
.= exp_R /. ((p (#) ln ) /. d) by A10, A12, PARTFUN2:6
.= exp_R . ((p (#) ln ) . d) by A13, PARTFUN1:def 8
.= exp_R . (p * (ln . d)) by A13, VALUED_1:def 5
.= exp_R . (p * (log number_e ,d)) by A12, Def2
.= exp_R . (log number_e ,(d to_power p)) by A14, Lm4, POWER:63
.= d to_power p by A14, Th15, POWER:39
.= d #R p by A14, POWER:def 2
.= (#R p) . d by A12, Def4 ; :: thesis: verum

end;

dom (#R p) = right_open_halfline 0 by Def4;
then ( x is Real & exp_R * (p (#) ln ) = #R p ) by A10, A11, PARTFUN1:34, XREAL_0:def 1;
hence ( x > 0 implies ( #R p is_differentiable_in x & diff (#R p),x = p * (x #R (p - 1)) ) ) by A2; :: thesis: verum