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:15;
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:15
.= p * (1 / x) by A6, Th18 ;
A9: exp_R is_differentiable_in (p (#) ln) . x by SIN_COS:65;
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:55
.= x to_power p by A3, Th15, POWER:34 ;
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:25
.= p * ((x to_power p) * (x to_power (- 1))) by A3, POWER:28
.= p * (x to_power (p + (- 1))) by A3, POWER:27
.= 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:27
.= 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 6
.= exp_R /. ((p (#) ln) /. d) by A10, A12, PARTFUN2:3
.= exp_R . ((p (#) ln) . d) by A13, PARTFUN1:def 6
.= 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:55
.= d to_power p by A14, Th15, POWER:34
.= 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:5, 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