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 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) ) )

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 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) ) )

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 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) ) )

let k be positive Real; :: thesis: 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) ) )

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

consider Fsq being Functional_Sequence of X,REAL such that

A1: 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) ) ) by Th62;

defpred S_{1}[ Nat, set ] means ex DMFSQN being Element of S st

( $2 = DMFSQN & ex FSQN being PartFunc of X,REAL st

( Fsq . $1 = FSQN & M . (DMFSQN `) = 0 & dom FSQN = DMFSQN & FSQN is DMFSQN -measurable & (abs FSQN) to_power k is_integrable_on M ) );

A2: for n being Element of NAT ex y being Element of S st S_{1}[n,y]

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

reconsider E0 = meet (rng G) as Element of S ;

A4: for n being Nat holds

( M . (X \ (G . n)) = 0 & E0 c= dom (Fsq . n) )

for A being set st A in X \ (rng G) holds

( A in S & A is measure_zero of M )

A in S ) & ( for A being set st A in X \ (rng G) holds

A is measure_zero of M ) ) ;

then X \ (rng G) c= S ;

then X \ (rng G) is N_Measure_fam of S by A6, MEASURE2:def 1;

then A12: union (X \ (rng G)) is measure_zero of M by A11, MEASURE2:14;

E0 ` = X \ (X \ (union (X \ (rng G)))) by MEASURE1:4

.= X /\ (union (X \ (rng G))) by XBOOLE_1:48

.= union (X \ (rng G)) by XBOOLE_1:28 ;

then A13: M . (E0 `) = 0 by A12, MEASURE1:def 7;

set Fsq2 = Fsq || E0;

A14: for n being Nat holds dom ((Fsq || E0) . n) = E0

take Fsq2 ; :: thesis: for n being Nat holds

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

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

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) ) )

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 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) ) )

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 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) ) )

let k be positive Real; :: thesis: 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) ) )

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

consider Fsq being Functional_Sequence of X,REAL such that

A1: 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) ) ) by Th62;

defpred S

( $2 = DMFSQN & ex FSQN being PartFunc of X,REAL st

( Fsq . $1 = FSQN & M . (DMFSQN `) = 0 & dom FSQN = DMFSQN & FSQN is DMFSQN -measurable & (abs FSQN) to_power k is_integrable_on M ) );

A2: for n being Element of NAT ex y being Element of S st S

proof

consider G being sequence of S such that
let n be Element of NAT ; :: thesis: ex y being Element of S st S_{1}[n,y]

Fsq . n in Lp_Functions (M,k) by A1;

then ex FMF being PartFunc of X,REAL st

( Fsq . n = FMF & ex ND being Element of S st

( M . (ND `) = 0 & dom FMF = ND & FMF is ND -measurable & (abs FMF) to_power k is_integrable_on M ) ) ;

hence ex y being Element of S st S_{1}[n,y]
; :: thesis: verum

end;Fsq . n in Lp_Functions (M,k) by A1;

then ex FMF being PartFunc of X,REAL st

( Fsq . n = FMF & ex ND being Element of S st

( M . (ND `) = 0 & dom FMF = ND & FMF is ND -measurable & (abs FMF) to_power k is_integrable_on M ) ) ;

hence ex y being Element of S st S

A3: for n being Element of NAT holds S

reconsider E0 = meet (rng G) as Element of S ;

A4: for n being Nat holds

( M . (X \ (G . n)) = 0 & E0 c= dom (Fsq . n) )

proof

A6:
X \ (rng G) is N_Sub_set_fam of X
by MEASURE1:21;
let n be Nat; :: thesis: ( M . (X \ (G . n)) = 0 & E0 c= dom (Fsq . n) )

A5: n in NAT by ORDINAL1:def 12;

ex D being Element of S st

( G . n = D & ex F being PartFunc of X,REAL st

( Fsq . n = F & M . (D `) = 0 & dom F = D & F is D -measurable & (abs F) to_power k is_integrable_on M ) ) by A3, A5;

hence ( M . (X \ (G . n)) = 0 & E0 c= dom (Fsq . n) ) by FUNCT_2:4, SETFAM_1:3, A5; :: thesis: verum

end;A5: n in NAT by ORDINAL1:def 12;

ex D being Element of S st

( G . n = D & ex F being PartFunc of X,REAL st

( Fsq . n = F & M . (D `) = 0 & dom F = D & F is D -measurable & (abs F) to_power k is_integrable_on M ) ) by A3, A5;

hence ( M . (X \ (G . n)) = 0 & E0 c= dom (Fsq . n) ) by FUNCT_2:4, SETFAM_1:3, A5; :: thesis: verum

for A being set st A in X \ (rng G) holds

( A in S & A is measure_zero of M )

proof

then A11:
( ( for A being object st A in X \ (rng G) holds
let A be set ; :: thesis: ( A in X \ (rng G) implies ( A in S & A is measure_zero of M ) )

assume A7: A in X \ (rng G) ; :: thesis: ( A in S & A is measure_zero of M )

then reconsider A0 = A as Subset of X ;

A0 ` in rng G by A7, SETFAM_1:def 7;

then consider n being object such that

A8: ( n in NAT & A0 ` = G . n ) by FUNCT_2:11;

reconsider n = n as Nat by A8;

A9: (A0 `) ` = A0 ;

then A0 = X \ (G . n) by A8;

hence A in S by MEASURE1:34; :: thesis: A is measure_zero of M

A10: M . A0 = 0 by A4, A8, A9;

A0 = X \ (G . n) by A8, A9;

then A is Element of S by MEASURE1:34;

hence A is measure_zero of M by A10, MEASURE1:def 7; :: thesis: verum

end;assume A7: A in X \ (rng G) ; :: thesis: ( A in S & A is measure_zero of M )

then reconsider A0 = A as Subset of X ;

A0 ` in rng G by A7, SETFAM_1:def 7;

then consider n being object such that

A8: ( n in NAT & A0 ` = G . n ) by FUNCT_2:11;

reconsider n = n as Nat by A8;

A9: (A0 `) ` = A0 ;

then A0 = X \ (G . n) by A8;

hence A in S by MEASURE1:34; :: thesis: A is measure_zero of M

A10: M . A0 = 0 by A4, A8, A9;

A0 = X \ (G . n) by A8, A9;

then A is Element of S by MEASURE1:34;

hence A is measure_zero of M by A10, MEASURE1:def 7; :: thesis: verum

A in S ) & ( for A being set st A in X \ (rng G) holds

A is measure_zero of M ) ) ;

then X \ (rng G) c= S ;

then X \ (rng G) is N_Measure_fam of S by A6, MEASURE2:def 1;

then A12: union (X \ (rng G)) is measure_zero of M by A11, MEASURE2:14;

E0 ` = X \ (X \ (union (X \ (rng G)))) by MEASURE1:4

.= X /\ (union (X \ (rng G))) by XBOOLE_1:48

.= union (X \ (rng G)) by XBOOLE_1:28 ;

then A13: M . (E0 `) = 0 by A12, MEASURE1:def 7;

set Fsq2 = Fsq || E0;

A14: for n being Nat holds dom ((Fsq || E0) . n) = E0

proof

let n be Nat; :: thesis: dom ((Fsq || E0) . n) = E0

dom ((Fsq || E0) . n) = dom ((Fsq . n) | E0) by MESFUN9C:def 1;

then dom ((Fsq || E0) . n) = (dom (Fsq . n)) /\ E0 by RELAT_1:61;

hence dom ((Fsq || E0) . n) = E0 by A4, XBOOLE_1:28; :: thesis: verum

end;dom ((Fsq || E0) . n) = dom ((Fsq . n) | E0) by MESFUN9C:def 1;

then dom ((Fsq || E0) . n) = (dom (Fsq . n)) /\ E0 by RELAT_1:61;

hence dom ((Fsq || E0) . n) = E0 by A4, XBOOLE_1:28; :: thesis: verum

now :: thesis: for n, m being Nat holds dom ((Fsq || E0) . n) = dom ((Fsq || E0) . m)

then reconsider Fsq2 = Fsq || E0 as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;let n, m be Nat; :: thesis: dom ((Fsq || E0) . n) = dom ((Fsq || E0) . m)

( dom ((Fsq || E0) . n) = E0 & dom ((Fsq || E0) . m) = E0 ) by A14;

hence dom ((Fsq || E0) . n) = dom ((Fsq || E0) . m) ; :: thesis: verum

end;( dom ((Fsq || E0) . n) = E0 & dom ((Fsq || E0) . m) = E0 ) by A14;

hence dom ((Fsq || E0) . n) = dom ((Fsq || E0) . m) ; :: thesis: verum

take Fsq2 ; :: thesis: for n being Nat holds

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

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

hereby :: thesis: verum

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

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

Fsq . n in Lp_Functions (M,k) by A1;

then A15: ex FMF being PartFunc of X,REAL st

( Fsq . n = FMF & ex ND being Element of S st

( M . (ND `) = 0 & dom FMF = ND & FMF is ND -measurable & (abs FMF) to_power k is_integrable_on M ) ) ;

then reconsider E2 = dom (Fsq . n) as Element of S ;

A16: E2 /\ E0 = E0 by A4, XBOOLE_1:28;

R_EAL (Fsq . n) is E2 -measurable by A15;

then R_EAL (Fsq . n) is E0 -measurable by A4, MESFUNC1:30;

then Fsq . n is E0 -measurable ;

then (Fsq . n) | E0 is E0 -measurable by A16, MESFUNC6:76;

then A17: Fsq2 . n is E0 -measurable by MESFUN9C:def 1;

A18: dom (Fsq2 . n) = E0 by A14;

( dom ((abs (Fsq . n)) to_power k) = dom (abs (Fsq . n)) & dom ((abs (Fsq2 . n)) to_power k) = dom (abs (Fsq2 . n)) ) by MESFUN6C:def 4;

then A19: ( dom ((abs (Fsq . n)) to_power k) = dom (Fsq . n) & dom ((abs (Fsq2 . n)) to_power k) = dom (Fsq2 . n) ) by VALUED_1:def 11;

for x being object st x in dom ((abs (Fsq2 . n)) to_power k) holds

((abs (Fsq2 . n)) to_power k) . x = ((abs (Fsq . n)) to_power k) . x

then (abs (Fsq2 . n)) to_power k is_integrable_on M by A15, MESFUNC6:91;

hence A22: Fsq2 . n in Lp_Functions (M,k) by A17, A18, A13; :: thesis: ( Fsq2 . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq2 . n),M,k) & ex r being Real st

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

A23: ( Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) ) by A1;

reconsider EB = E0 ` as Element of S by MEASURE1:34;

(Fsq2 . n) | (EB `) = Fsq2 . n by A18, RELAT_1:68;

then (Fsq2 . n) | (EB `) = (Fsq . n) | (EB `) by MESFUN9C:def 1;

then A24: Fsq2 . n a.e.= Fsq . n,M by A13;

hence Fsq2 . n in Sq . n by A23, A22, Th36; :: thesis: ( Sq . n = a.e-eq-class_Lp ((Fsq2 . n),M,k) & ex r being Real st

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

a.e-eq-class_Lp ((Fsq2 . n),M,k) = a.e-eq-class_Lp ((Fsq . n),M,k) by Th42, A24;

hence Sq . n = a.e-eq-class_Lp ((Fsq2 . n),M,k) by A1; :: thesis: ex r being Real st

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

hence ex r being Real st

( 0 <= r & r = Integral (M,((abs (Fsq2 . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) by Th53, Th38, A22; :: thesis: verum

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

Fsq . n in Lp_Functions (M,k) by A1;

then A15: ex FMF being PartFunc of X,REAL st

( Fsq . n = FMF & ex ND being Element of S st

( M . (ND `) = 0 & dom FMF = ND & FMF is ND -measurable & (abs FMF) to_power k is_integrable_on M ) ) ;

then reconsider E2 = dom (Fsq . n) as Element of S ;

A16: E2 /\ E0 = E0 by A4, XBOOLE_1:28;

R_EAL (Fsq . n) is E2 -measurable by A15;

then R_EAL (Fsq . n) is E0 -measurable by A4, MESFUNC1:30;

then Fsq . n is E0 -measurable ;

then (Fsq . n) | E0 is E0 -measurable by A16, MESFUNC6:76;

then A17: Fsq2 . n is E0 -measurable by MESFUN9C:def 1;

A18: dom (Fsq2 . n) = E0 by A14;

( dom ((abs (Fsq . n)) to_power k) = dom (abs (Fsq . n)) & dom ((abs (Fsq2 . n)) to_power k) = dom (abs (Fsq2 . n)) ) by MESFUN6C:def 4;

then A19: ( dom ((abs (Fsq . n)) to_power k) = dom (Fsq . n) & dom ((abs (Fsq2 . n)) to_power k) = dom (Fsq2 . n) ) by VALUED_1:def 11;

for x being object st x in dom ((abs (Fsq2 . n)) to_power k) holds

((abs (Fsq2 . n)) to_power k) . x = ((abs (Fsq . n)) to_power k) . x

proof

then
((abs (Fsq . n)) to_power k) | E0 = (abs (Fsq2 . n)) to_power k
by A14, A16, A19, FUNCT_1:46;
let x be object ; :: thesis: ( x in dom ((abs (Fsq2 . n)) to_power k) implies ((abs (Fsq2 . n)) to_power k) . x = ((abs (Fsq . n)) to_power k) . x )

assume A20: x in dom ((abs (Fsq2 . n)) to_power k) ; :: thesis: ((abs (Fsq2 . n)) to_power k) . x = ((abs (Fsq . n)) to_power k) . x

then reconsider x0 = x as Element of X ;

A21: x in dom ((abs (Fsq . n)) to_power k) by A18, A19, A16, A20, XBOOLE_0:def 4;

thus ((abs (Fsq2 . n)) to_power k) . x = ((abs (Fsq2 . n)) . x0) to_power k by A20, MESFUN6C:def 4

.= |.((Fsq2 . n) . x0).| to_power k by VALUED_1:18

.= |.(((Fsq . n) | E0) . x0).| to_power k by MESFUN9C:def 1

.= |.((Fsq . n) . x0).| to_power k by A18, A19, A20, FUNCT_1:49

.= ((abs (Fsq . n)) . x0) to_power k by VALUED_1:18

.= ((abs (Fsq . n)) to_power k) . x by A21, MESFUN6C:def 4 ; :: thesis: verum

end;assume A20: x in dom ((abs (Fsq2 . n)) to_power k) ; :: thesis: ((abs (Fsq2 . n)) to_power k) . x = ((abs (Fsq . n)) to_power k) . x

then reconsider x0 = x as Element of X ;

A21: x in dom ((abs (Fsq . n)) to_power k) by A18, A19, A16, A20, XBOOLE_0:def 4;

thus ((abs (Fsq2 . n)) to_power k) . x = ((abs (Fsq2 . n)) . x0) to_power k by A20, MESFUN6C:def 4

.= |.((Fsq2 . n) . x0).| to_power k by VALUED_1:18

.= |.(((Fsq . n) | E0) . x0).| to_power k by MESFUN9C:def 1

.= |.((Fsq . n) . x0).| to_power k by A18, A19, A20, FUNCT_1:49

.= ((abs (Fsq . n)) . x0) to_power k by VALUED_1:18

.= ((abs (Fsq . n)) to_power k) . x by A21, MESFUN6C:def 4 ; :: thesis: verum

then (abs (Fsq2 . n)) to_power k is_integrable_on M by A15, MESFUNC6:91;

hence A22: Fsq2 . n in Lp_Functions (M,k) by A17, A18, A13; :: thesis: ( Fsq2 . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq2 . n),M,k) & ex r being Real st

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

A23: ( Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) ) by A1;

reconsider EB = E0 ` as Element of S by MEASURE1:34;

(Fsq2 . n) | (EB `) = Fsq2 . n by A18, RELAT_1:68;

then (Fsq2 . n) | (EB `) = (Fsq . n) | (EB `) by MESFUN9C:def 1;

then A24: Fsq2 . n a.e.= Fsq . n,M by A13;

hence Fsq2 . n in Sq . n by A23, A22, Th36; :: thesis: ( Sq . n = a.e-eq-class_Lp ((Fsq2 . n),M,k) & ex r being Real st

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

a.e-eq-class_Lp ((Fsq2 . n),M,k) = a.e-eq-class_Lp ((Fsq . n),M,k) by Th42, A24;

hence Sq . n = a.e-eq-class_Lp ((Fsq2 . n),M,k) by A1; :: thesis: ex r being Real st

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

hence ex r being Real st

( 0 <= r & r = Integral (M,((abs (Fsq2 . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) by Th53, Th38, A22; :: thesis: verum