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₁[ 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₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of PFuncs (X,REAL) st S₁[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₁[x,y] by A2, Th38; :: thesis: verum

end;

consider G being sequence of (PFuncs (X,REAL)) such that
A3: for n being Element of NAT holds S₁[n,G . n] from FUNCT_2:sch 3(A1);
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) ) )

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;

hence 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) ) ) ; :: thesis: verum