theorem Th47: :: LPSPACC1:47

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M holds
Integral (M,|.(f + g).|) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|))