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

proof

let n be Element of NAT ; :: thesis: ex y being Element of S st S₁[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₁[n,y] ; :: thesis: verum

end;

consider G being sequence of S such that
A3: for n being Element of NAT holds S₁[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) )

proof

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;

A6: X \ (rng G) is N_Sub_set_fam of X by MEASURE1:21;
for A being set st A in X \ (rng G) holds
( A in S & A is measure_zero of M )

proof

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;

then A11: ( ( for A being object st A in X \ (rng G) holds
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;

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

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;

then reconsider Fsq2 = Fsq || E0 as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
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

proof

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;

then ((abs (Fsq . n)) to_power k) | E0 = (abs (Fsq2 . n)) to_power k by A14, A16, A19, FUNCT_1:46;
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;