for X being non empty set
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