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) (#) (f 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) (#) (f 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) (#) (f to_power b) = f to_power (a + b) )
assume A1: ( f is nonnegative & a > 0 & b > 0 ) ; :: thesis: (f to_power a) (#) (f to_power b) = f to_power (a + b)
A2: ( dom (f to_power a) = dom f & dom (f to_power b) = dom f ) by MESFUN6C:def 4;
A3: dom ((f to_power a) (#) (f to_power b)) = (dom (f to_power a)) /\ (dom (f to_power b)) by VALUED_1:def 4;
then A4: dom ((f to_power a) (#) (f to_power b)) = dom (f to_power (a + b)) by A2, MESFUN6C:def 4;
for x being object st x in dom ((f to_power a) (#) (f to_power b)) holds
((f to_power a) (#) (f to_power b)) . x = (f to_power (a + b)) . x

proof

let x be object ; :: thesis: ( x in dom ((f to_power a) (#) (f to_power b)) implies ((f to_power a) (#) (f to_power b)) . x = (f to_power (a + b)) . x )
assume A5: x in dom ((f to_power a) (#) (f to_power b)) ; :: thesis: ((f to_power a) (#) (f to_power b)) . x = (f to_power (a + b)) . x
then ( (f to_power a) . x = (f . x) to_power a & (f to_power b) . x = (f . x) to_power b ) by A2, A3, MESFUN6C:def 4;
then A6: ((f to_power a) (#) (f to_power b)) . x = ((f . x) to_power a) * ((f . x) to_power b) by A5, VALUED_1:def 4;
A7: (f to_power (a + b)) . x = (f . x) to_power (a + b) by A4, A5, MESFUN6C:def 4;
then A8: ( f . x > 0 implies ((f to_power a) (#) (f to_power b)) . x = (f to_power (a + b)) . x ) by A6, POWER:27;

now :: thesis: ( f . x = 0 implies ((f to_power a) (#) (f to_power b)) . x = (f to_power (a + b)) . x )

assume A9: f . x = 0 ; :: thesis: ((f to_power a) (#) (f to_power b)) . x = (f to_power (a + b)) . x
then ((f to_power a) (#) (f to_power b)) . x = 0 * (0 to_power b) by A1, A6, POWER:def 2;
hence ((f to_power a) (#) (f to_power b)) . x = (f to_power (a + b)) . x by A7, A1, A9, POWER:def 2; :: thesis: verum

end;

hence ((f to_power a) (#) (f to_power b)) . x = (f to_power (a + b)) . x by A1, A8, MESFUNC6:51; :: thesis: verum

end;

hence (f to_power a) (#) (f to_power b) = f to_power (a + b) by A4, FUNCT_1:2; :: thesis: verum