let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let k be positive Real; :: thesis:
let Sq be sequence of (Lp-Space M,k); :: thesis:
consider Fsq being Functional_Sequence of X,REAL such that
A1: 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) ) ) by Th004X;
defpred S₁[ Element of 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_measurable_on DMFSQN & (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]

let n be Element of NAT ; :: thesis:
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_measurable_on ND & (abs FMF) to_power k is_integrable_on M ) ) ;
hence ex y being Element of S st S₁[n,y] ; :: thesis:

end;

consider G being Function of NAT ,S such that
A3: for n being Element of NAT holds S₁[n,G . n] from FUNCT_2:sch 10(A2);
reconsider E0 = meet (rng G) as Element of S ;
A4: for n being Element of NAT holds
( M . (X \ (G . n)) = 0 & E0 c= dom (Fsq . n) )

let n be Element of NAT ; :: thesis:
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_measurable_on D & (abs F) to_power k is_integrable_on M ) ) by A3;
hence ( M . (X \ (G . n)) = 0 & E0 c= dom (Fsq . n) ) by FUNCT_2:6, SETFAM_1:4; :: thesis:

end;

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

let A be set ; :: thesis:
assume B11: A in X \ (rng G) ; :: thesis:
then reconsider A0 = A as Subset of X ;
A0 ` in rng G by B11, SETFAM_1:def 8;
then consider n being set such that
B12: ( n in NAT & A0 ` = G . n ) by FUNCT_2:17;
reconsider n = n as Element of NAT by B12;
B13: (A0 ` ) ` = A0 ;
then A0 = X \ (G . n) by B12;
hence A in S by MEASURE1:66; :: thesis:
B14: M . A0 = 0 by A4, B12, B13;
A0 = X \ (G . n) by B12, B13;
then A is Element of S by MEASURE1:66;
hence A is measure_zero of M by B14, MEASURE1:def 13; :: thesis:

end;

then B2: ( ( for A being set 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 by TARSKI:def 3;
then X \ (rng G) is N_Measure_fam of S by B1, MEASURE2:def 1;
then B3: union (X \ (rng G)) is measure_zero of M by B2, MEASURE2:16;
E0 ` = X \ (X \ (union (X \ (rng G)))) by MEASURE1:15
.= X /\ (union (X \ (rng G))) by XBOOLE_1:48
.= union (X \ (rng G)) by XBOOLE_1:28 ;
then B4: M . (E0 ` ) = 0 by B3, MEASURE1:def 13;
set Fsq2 = Fsq || E0;
A5: for n being Element of NAT holds dom ((Fsq || E0) . n) = E0

let n be Element of NAT ; :: thesis:
dom ((Fsq || E0) . n) = dom ((Fsq . n) | E0) by MESFUN9C:def 1;
then dom ((Fsq || E0) . n) = (dom (Fsq . n)) /\ E0 by RELAT_1:90;
hence dom ((Fsq || E0) . n) = E0 by A4, XBOOLE_1:28; :: thesis:

end;

let n, m be natural number ; :: thesis:
( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 13;
then ( dom ((Fsq || E0) . n) = E0 & dom ((Fsq || E0) . m) = E0 ) by A5;
hence dom ((Fsq || E0) . n) = dom ((Fsq || E0) . m) ; :: thesis:

end;

then reconsider Fsq2 = Fsq || E0 as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
take Fsq2 ; :: thesis:

let x be set ; :: thesis:
assume L1: x in dom ((abs (Fsq2 . n)) to_power k) ; :: thesis:
then reconsider x0 = x as Element of X ;
L2: x in dom ((abs (Fsq . n)) to_power k) by A10, A11, A8, L1, XBOOLE_0:def 4;
thus ((abs (Fsq2 . n)) to_power k) . x = ((abs (Fsq2 . n)) . x0) to_power k by L1, MESFUN6C:def 6
.= (abs ((Fsq2 . n) . x0)) to_power k by VALUED_1:18
.= (abs (((Fsq . n) | E0) . x0)) to_power k by MESFUN9C:def 1
.= (abs ((Fsq . n) . x0)) to_power k by A10, A11, L1, FUNCT_1:72
.= ((abs (Fsq . n)) . x0) to_power k by VALUED_1:18
.= ((abs (Fsq . n)) to_power k) . x by L2, MESFUN6C:def 6 ; :: thesis:

end;

end;