theorem Th63: :: LPSPACE2:63

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real
for Sq being sequence of (Lp-Space (M,k)) ex Fsq being with_the_same_dom Functional_Sequence of X,REAL st
for n being Nat holds
( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )