let X be non empty set ; :: thesis: 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 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for k being positive Real

for Sq being sequence of (Lp-Space (M,k)) ex Fsq being 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

let M be sigma_Measure of S; :: thesis: for k being positive Real

for Sq being sequence of (Lp-Space (M,k)) ex Fsq being 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

let k be positive Real; :: thesis: for Sq being sequence of (Lp-Space (M,k)) ex Fsq being 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

let Sq be sequence of (Lp-Space (M,k)); :: thesis: ex Fsq being 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

defpred S_{1}[ Nat, set ] means ex f being PartFunc of X,REAL st

( $2 = f & f in Lp_Functions (M,k) & f in Sq . $1 & Sq . $1 = a.e-eq-class_Lp (f,M,k) & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & ||.(Sq . $1).|| = r to_power (1 / k) ) );

A1: for x being Element of NAT ex y being Element of PFuncs (X,REAL) st S_{1}[x,y]

A3: for n being Element of NAT holds S_{1}[n,G . n]
from FUNCT_2:sch 3(A1);

reconsider G = G as Functional_Sequence of X,REAL ;

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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) ) ; :: thesis: verum

for M being sigma_Measure of S

for k being positive Real

for Sq being sequence of (Lp-Space (M,k)) ex Fsq being 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for k being positive Real

for Sq being sequence of (Lp-Space (M,k)) ex Fsq being 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

let M be sigma_Measure of S; :: thesis: for k being positive Real

for Sq being sequence of (Lp-Space (M,k)) ex Fsq being 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

let k be positive Real; :: thesis: for Sq being sequence of (Lp-Space (M,k)) ex Fsq being 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

let Sq be sequence of (Lp-Space (M,k)); :: thesis: ex Fsq being 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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

defpred S

( $2 = f & f in Lp_Functions (M,k) & f in Sq . $1 & Sq . $1 = a.e-eq-class_Lp (f,M,k) & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & ||.(Sq . $1).|| = r to_power (1 / k) ) );

A1: for x being Element of NAT ex y being Element of PFuncs (X,REAL) st S

proof

consider G being sequence of (PFuncs (X,REAL)) such that
let x be Element of NAT ; :: thesis: ex y being Element of PFuncs (X,REAL) st S_{1}[x,y]

consider y being PartFunc of X,REAL such that

A2: ( y in Lp_Functions (M,k) & Sq . x = a.e-eq-class_Lp (y,M,k) ) by Th53;

ex r being Real st

( 0 <= r & r = Integral (M,((abs y) to_power k)) & ||.(Sq . x).|| = r to_power (1 / k) ) by Th53, A2, Th38;

hence ex y being Element of PFuncs (X,REAL) st S_{1}[x,y]
by A2, Th38; :: thesis: verum

end;consider y being PartFunc of X,REAL such that

A2: ( y in Lp_Functions (M,k) & Sq . x = a.e-eq-class_Lp (y,M,k) ) by Th53;

ex r being Real st

( 0 <= r & r = Integral (M,((abs y) to_power k)) & ||.(Sq . x).|| = r to_power (1 / k) ) by Th53, A2, Th38;

hence ex y being Element of PFuncs (X,REAL) st S

A3: for n being Element of NAT holds S

reconsider G = G as Functional_Sequence of X,REAL ;

now :: thesis: for n being Nat holds

( G . n in Lp_Functions (M,k) & G . n in Sq . n & Sq . n = a.e-eq-class_Lp ((G . n),M,k) & ex r being Real st

( r = Integral (M,((abs (G . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

hence
ex Fsq being Functional_Sequence of X,REAL st ( G . n in Lp_Functions (M,k) & G . n in Sq . n & Sq . n = a.e-eq-class_Lp ((G . n),M,k) & ex r being Real st

( r = Integral (M,((abs (G . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

let n be Nat; :: thesis: ( G . n in Lp_Functions (M,k) & G . n in Sq . n & Sq . n = a.e-eq-class_Lp ((G . n),M,k) & ex r being Real st

( r = Integral (M,((abs (G . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

n in NAT by ORDINAL1:def 12;

then ex f being PartFunc of X,REAL st

( G . n = f & f in Lp_Functions (M,k) & f in Sq . n & Sq . n = a.e-eq-class_Lp (f,M,k) & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) ) by A3;

hence ( G . n in Lp_Functions (M,k) & G . n in Sq . n & Sq . n = a.e-eq-class_Lp ((G . n),M,k) & ex r being Real st

( r = Integral (M,((abs (G . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) ) ; :: thesis: verum

end;( r = Integral (M,((abs (G . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

n in NAT by ORDINAL1:def 12;

then ex f being PartFunc of X,REAL st

( G . n = f & f in Lp_Functions (M,k) & f in Sq . n & Sq . n = a.e-eq-class_Lp (f,M,k) & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) ) by A3;

hence ( G . n in Lp_Functions (M,k) & G . n in Sq . n & Sq . n = a.e-eq-class_Lp ((G . n),M,k) & ex r being Real st

( r = Integral (M,((abs (G . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) ) ; :: thesis: verum

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

( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) ) ; :: thesis: verum