theorem Th23: :: LPSPACE2:23

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real holds
( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) )