let X be non empty set ; :: thesis: for a, b being Real
for f being PartFunc of X,REAL st f is nonnegative & a > 0 & b > 0 holds
(f to_power a) to_power b = f to_power (a * b)
let a, b be Real; :: thesis: for f being PartFunc of X,REAL st f is nonnegative & a > 0 & b > 0 holds
(f to_power a) to_power b = f to_power (a * b)
let f be PartFunc of X,REAL ; :: thesis: ( f is nonnegative & a > 0 & b > 0 implies (f to_power a) to_power b = f to_power (a * b) )
assume AS: ( f is nonnegative & a > 0 & b > 0 ) ; :: thesis: (f to_power a) to_power b = f to_power (a * b)
A1: ( dom (f to_power a) = dom f & dom ((f to_power a) to_power b) = dom (f to_power a) & dom (f to_power (a * b)) = dom f ) by MESFUN6C:def 6;
for x being set st x in dom ((f to_power a) to_power b) holds
((f to_power a) to_power b) . x = (f to_power (a * b)) . x

proof

let x be set ; :: thesis: ( x in dom ((f to_power a) to_power b) implies ((f to_power a) to_power b) . x = (f to_power (a * b)) . x )
assume A6: x in dom ((f to_power a) to_power b) ; :: thesis: ((f to_power a) to_power b) . x = (f to_power (a * b)) . x
then A7: ((f to_power a) to_power b) . x = ((f to_power a) . x) to_power b by MESFUN6C:def 6
.= ((f . x) to_power a) to_power b by A1, A6, MESFUN6C:def 6 ;
A8: (f to_power (a * b)) . x = (f . x) to_power (a * b) by A1, A6, MESFUN6C:def 6;
then A9: ( f . x > 0 implies ((f to_power a) to_power b) . x = (f to_power (a * b)) . x ) by A7, POWER:38;

now

assume C1: f . x = 0 ; :: thesis: ((f to_power a) to_power b) . x = (f to_power (a * b)) . x
then ((f to_power a) to_power b) . x = 0 to_power b by AS, A7, POWER:def 2;
then ((f to_power a) to_power b) . x = 0 by AS, POWER:def 2;
hence ((f to_power a) to_power b) . x = (f to_power (a * b)) . x by AS, C1, A8, POWER:def 2; :: thesis: verum

end;

hence ((f to_power a) to_power b) . x = (f to_power (a * b)) . x by A9, AS, MESFUNC6:51; :: thesis: verum

end;

hence (f to_power a) to_power b = f to_power (a * b) by A1, FUNCT_1:9; :: thesis: verum