let X be non empty set ; :: thesis: for k being Real st k > 0 holds
for f, g being PartFunc of X,REAL
for x being Element of X st x in (dom f) /\ (dom g) holds
((abs (f + g)) to_power k) . x <= ((2 to_power k) (#) (((abs f) to_power k) + ((abs g) to_power k))) . x
let k be Element of REAL ; :: thesis: ( k > 0 implies for f, g being PartFunc of X,REAL
for x being Element of X st x in (dom f) /\ (dom g) holds
((abs (f + g)) to_power k) . x <= ((2 to_power k) (#) (((abs f) to_power k) + ((abs g) to_power k))) . x )
assume A1: k > 0 ; :: thesis: for f, g being PartFunc of X,REAL
for x being Element of X st x in (dom f) /\ (dom g) holds
((abs (f + g)) to_power k) . x <= ((2 to_power k) (#) (((abs f) to_power k) + ((abs g) to_power k))) . x
let f, g be PartFunc of X,REAL ; :: thesis: for x being Element of X st x in (dom f) /\ (dom g) holds
((abs (f + g)) to_power k) . x <= ((2 to_power k) (#) (((abs f) to_power k) + ((abs g) to_power k))) . x
let x be Element of X; :: thesis: ( x in (dom f) /\ (dom g) implies ((abs (f + g)) to_power k) . x <= ((2 to_power k) (#) (((abs f) to_power k) + ((abs g) to_power k))) . x )
assume A2: x in (dom f) /\ (dom g) ; :: thesis: ((abs (f + g)) to_power k) . x <= ((2 to_power k) (#) (((abs f) to_power k) + ((abs g) to_power k))) . x
A3: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then dom (abs (f + g)) = (dom f) /\ (dom g) by VALUED_1:def 11;
then x in dom ((abs (f + g)) to_power k) by A2, MESFUN6C:def 6;
then A5: ((abs (f + g)) to_power k) . x = ((abs (f + g)) . x) to_power k by MESFUN6C:def 6
.= (abs ((f + g) . x)) to_power k by VALUED_1:18
.= (abs ((f . x) + (g . x))) to_power k by A3, A2, VALUED_1:def 1 ;
( dom (abs f) = dom f & dom (abs g) = dom g ) by VALUED_1:def 11;
then ( x in dom (abs f) & x in dom (abs g) ) by A2, XBOOLE_0:def 4;
then A6: ( x in dom ((abs f) to_power k) & x in dom ((abs g) to_power k) ) by MESFUN6C:def 6;
( (abs (f . x)) to_power k = ((abs f) . x) to_power k & (abs (g . x)) to_power k = ((abs g) . x) to_power k ) by VALUED_1:18;
then A7: ( (abs (f . x)) to_power k = ((abs f) to_power k) . x & (abs (g . x)) to_power k = ((abs g) to_power k) . x ) by A6, MESFUN6C:def 6;
dom (((abs f) to_power k) + ((abs g) to_power k)) = (dom ((abs f) to_power k)) /\ (dom ((abs g) to_power k)) by VALUED_1:def 1;
then x in dom (((abs f) to_power k) + ((abs g) to_power k)) by A6, XBOOLE_0:def 4;
then (2 to_power k) * (((abs (f . x)) to_power k) + ((abs (g . x)) to_power k)) = (2 to_power k) * ((((abs f) to_power k) + ((abs g) to_power k)) . x) by A7, VALUED_1:def 1
.= ((2 to_power k) (#) (((abs f) to_power k) + ((abs g) to_power k))) . x by VALUED_1:6 ;
hence ((abs (f + g)) to_power k) . x <= ((2 to_power k) (#) (((abs f) to_power k) + ((abs g) to_power k))) . x by A1, A5, Lm005; :: thesis: verum