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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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₁[ Element of 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) ) );
A2: 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
A21: ( y in Lp_Functions M,k & Sq . x = a.e-eq-class_Lp y,M,k ) by Lm17x;
ex r being Real st
( 0 <= r & r = Integral M,((abs y) to_power k) & ||.(Sq . x).|| = r to_power (1 / k) ) by Lm17x, A21, EQC01;
hence ex y being Element of PFuncs X,REAL st S₁[x,y] by A21, EQC01; :: thesis: verum

end;

consider G being Function of NAT ,(PFuncs X,REAL ) such that
A3: for n being Element of NAT holds S₁[n,G . n] from FUNCT_2:sch 10(A2);
reconsider G = G as Functional_Sequence of X,REAL ;

now

let n be Element of 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) ) )
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 Element of 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