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 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 4;
then A4: ((abs (f + g)) to_power k) . x = ((abs (f + g)) . x) to_power k by MESFUN6C:def 4
.= |.((f + g) . x).| to_power k by VALUED_1:18
.= |.((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 A5: ( x in dom ((abs f) to_power k) & x in dom ((abs g) to_power k) ) by MESFUN6C:def 4;
( |.(f . x).| to_power k = ((abs f) . x) to_power k & |.(g . x).| to_power k = ((abs g) . x) to_power k ) by VALUED_1:18;
then A6: ( |.(f . x).| to_power k = ((abs f) to_power k) . x & |.(g . x).| to_power k = ((abs g) to_power k) . x ) by A5, MESFUN6C:def 4;
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 A5, XBOOLE_0:def 4;
then (2 to_power k) * ((|.(f . x).| to_power k) + (|.(g . x).| to_power k)) = (2 to_power k) * ((((abs f) to_power k) + ((abs g) to_power k)) . x) by A6, 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, A4, Th21; :: thesis: verum