let p, x be Real; :: thesis: ( x > 0 implies ( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) ) )
set f = #R p;
A1: 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 A2: x > 0 ; :: thesis: ( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) )
A3: ln is_differentiable_in x by A2, Th18;
then A4: p (#) ln is_differentiable_in x by FDIFF_1:15;
x in { g where g is Real : 0 < g } by A2;
then A5: x in right_open_halfline 0 by XXREAL_1:230;
then A6: x in dom (p (#) ln) by Th18, VALUED_1:def 5;
A7: diff ((p (#) ln),x) = p * (diff (ln,x)) by A3, FDIFF_1:15
.= p * (1 / x) by A5, Th18 ;
A8: exp_R is_differentiable_in (p (#) ln) . x by SIN_COS:65;
hence exp_R * (p (#) ln) is_differentiable_in x by A4, 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 A6, VALUED_1:def 5
.= exp_R . (p * (log (number_e,x))) by A5, Def2
.= exp_R . (log (number_e,(x to_power p))) by A2, Lm4, POWER:55
.= x to_power p by A2, Th15, POWER:34 ;
hence diff ((exp_R * (p (#) ln)),x) = (x to_power p) * (p * (1 / x)) by A4, A8, A7, 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 A2, POWER:28
.= p * (x to_power (p + (- 1))) by A2, POWER:27
.= p * (x #R (p - 1)) by A2, POWER:def 2 ;
:: thesis: verum

end;

rng (p (#) ln) c= dom exp_R by Th16;
then A9: dom (exp_R * (p (#) ln)) = dom (p (#) ln) by RELAT_1:27
.= right_open_halfline 0 by Th18, VALUED_1:def 5 ;
A10: 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 A11: d in right_open_halfline 0 ; :: thesis: (exp_R * (p (#) ln)) . d = (#R p) . d
A12: d in dom (p (#) ln) by A11, Th18, VALUED_1:def 5;
d in { g where g is Real : 0 < g } by A11, XXREAL_1:230;
then A13: ex g being Real st
( g = d & g > 0 ) ;
thus (exp_R * (p (#) ln)) . d = (exp_R * (p (#) ln)) /. d by A9, A11, PARTFUN1:def 6
.= exp_R /. ((p (#) ln) /. d) by A9, A11, PARTFUN2:3
.= exp_R . ((p (#) ln) . d) by A12, PARTFUN1:def 6
.= exp_R . (p * (ln . d)) by A12, VALUED_1:def 5
.= exp_R . (p * (log (number_e,d))) by A11, Def2
.= exp_R . (log (number_e,(d to_power p))) by A13, Lm4, POWER:55
.= d to_power p by A13, Th15, POWER:34
.= d #R p by A13, POWER:def 2
.= (#R p) . d by A11, Def4 ; :: thesis: verum

end;

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