let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for a, b being Real st b > 0 holds
(|.a.| to_power b) (#) ((abs f) to_power b) = (abs (a (#) f)) to_power b
let f be PartFunc of X,REAL; :: thesis: for a, b being Real st b > 0 holds
(|.a.| to_power b) (#) ((abs f) to_power b) = (abs (a (#) f)) to_power b
let a, b be Real; :: thesis: ( b > 0 implies (|.a.| to_power b) (#) ((abs f) to_power b) = (abs (a (#) f)) to_power b )
assume A1: b > 0 ; :: thesis: (|.a.| to_power b) (#) ((abs f) to_power b) = (abs (a (#) f)) to_power b
A2: ( dom ((|.a.| to_power b) (#) ((abs f) to_power b)) = dom ((abs f) to_power b) & dom (a (#) f) = dom f ) by VALUED_1:def 5;
A3: ( dom ((abs f) to_power b) = dom (abs f) & dom (abs (a (#) f)) = dom ((abs (a (#) f)) to_power b) ) by MESFUN6C:def 4;
A4: ( dom (abs f) = dom f & dom (abs (a (#) f)) = dom (a (#) f) ) by VALUED_1:def 11;
for x being Element of X st x in dom ((|.a.| to_power b) (#) ((abs f) to_power b)) holds
((|.a.| to_power b) (#) ((abs f) to_power b)) . x = ((abs (a (#) f)) to_power b) . x

proof

let x be Element of X; :: thesis: ( x in dom ((|.a.| to_power b) (#) ((abs f) to_power b)) implies ((|.a.| to_power b) (#) ((abs f) to_power b)) . x = ((abs (a (#) f)) to_power b) . x )
assume A5: x in dom ((|.a.| to_power b) (#) ((abs f) to_power b)) ; :: thesis: ((|.a.| to_power b) (#) ((abs f) to_power b)) . x = ((abs (a (#) f)) to_power b) . x
A6: ( |.(f . x).| >= 0 & |.a.| >= 0 ) by COMPLEX1:46;
((|.a.| to_power b) (#) ((abs f) to_power b)) . x = (|.a.| to_power b) * (((abs f) to_power b) . x) by A5, VALUED_1:def 5
.= (|.a.| to_power b) * (((abs f) . x) to_power b) by A2, A5, MESFUN6C:def 4
.= (|.a.| to_power b) * (|.(f . x).| to_power b) by VALUED_1:18
.= (|.a.| * |.(f . x).|) to_power b by A1, A6, Th5
.= |.(a * (f . x)).| to_power b by COMPLEX1:65
.= |.((a (#) f) . x).| to_power b by VALUED_1:6
.= ((abs (a (#) f)) . x) to_power b by VALUED_1:18 ;
hence ((|.a.| to_power b) (#) ((abs f) to_power b)) . x = ((abs (a (#) f)) to_power b) . x by A2, A3, A4, A5, MESFUN6C:def 4; :: thesis: verum

end;

hence (|.a.| to_power b) (#) ((abs f) to_power b) = (abs (a (#) f)) to_power b by A2, A3, A4, PARTFUN1:5; :: thesis: verum