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)) ) )
A1: ( x is Real & p is Real ) by XREAL_0:def 1;
set f = #R p;
A2: dom (#R p) = right_open_halfline 0 by Def4;
A3: 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 A4: x > 0 ; :: thesis: ( exp_R * (p (#) ln ) is_differentiable_in x & diff (exp_R * (p (#) ln )),x = p * (x #R (p - 1)) )
A5: x in right_open_halfline 0

proof

x in { g where g is Real : 0 < g } by A4;
hence x in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum

end;

then A6: x in dom (p (#) ln ) by Th18, VALUED_1:def 5;
A7: ln is_differentiable_in x by A4, Th18;
then A8: p (#) ln is_differentiable_in x by A1, FDIFF_1:23;
A9: exp_R is_differentiable_in (p (#) ln ) . x by SIN_COS:70;
hence exp_R * (p (#) ln ) is_differentiable_in x by A8, FDIFF_2:13; :: thesis: diff (exp_R * (p (#) ln )),x = p * (x #R (p - 1))
A10: 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 A4, Lm4, POWER:63
.= x to_power p by A4, Th15, POWER:39 ;
diff (p (#) ln ),x = p * (diff ln ,x) by A1, A7, FDIFF_1:23
.= p * (1 / x) by A5, Th18 ;
hence diff (exp_R * (p (#) ln )),x = (x to_power p) * (p * (1 / x)) by A8, A9, A10, 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 A4, POWER:33
.= p * (x to_power (p + (- 1))) by A4, POWER:32
.= p * (x #R (p - 1)) by A4, POWER:def 2 ;
:: thesis: verum

end;

exp_R * (p (#) ln ) = #R p

proof

A11: dom (exp_R * (p (#) ln )) = right_open_halfline 0

proof

rng (p (#) ln ) c= dom exp_R by Th16;
hence dom (exp_R * (p (#) ln )) = dom (p (#) ln ) by RELAT_1:46
.= right_open_halfline 0 by Th18, VALUED_1:def 5 ;
:: thesis: verum

end;

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 consider g being Real such that
A14: ( g = d & g > 0 ) ;
thus (exp_R * (p (#) ln )) . d = (exp_R * (p (#) ln )) /. d by A11, A12, PARTFUN1:def 8
.= exp_R /. ((p (#) ln ) /. d) by A11, 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;

hence exp_R * (p (#) ln ) = #R p by A2, A11, PARTFUN1:34; :: thesis: verum

end;

hence ( x > 0 implies ( #R p is_differentiable_in x & diff (#R p),x = p * (x #R (p - 1)) ) ) by A1, A3; :: thesis: verum