let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for a, b being Real st a > 0 & b > 0 holds
(a to_power b) (#) ((abs f) to_power b) = (a (#) (abs f)) to_power b
let f be PartFunc of X,REAL; :: thesis: for a, b being Real st a > 0 & b > 0 holds
(a to_power b) (#) ((abs f) to_power b) = (a (#) (abs f)) to_power b
let a, b be Real; :: thesis: ( a > 0 & b > 0 implies (a to_power b) (#) ((abs f) to_power b) = (a (#) (abs f)) to_power b )
assume A1: ( a > 0 & b > 0 ) ; :: thesis: (a to_power b) (#) ((abs f) to_power b) = (a (#) (abs f)) to_power b
then A2: |.a.| = a by COMPLEX1:43;
then (a to_power b) (#) ((abs f) to_power b) = (abs (a (#) f)) to_power b by A1, Th18;
hence (a to_power b) (#) ((abs f) to_power b) = (a (#) (abs f)) to_power b by A2, RFUNCT_1:25; :: thesis: verum