let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for k being geq_than_1 Real
for Sq being sequence of (Lp-Space (M,k)) st Sq is Cauchy_sequence_by_Norm holds
Sq is convergent
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for k being geq_than_1 Real
for Sq being sequence of (Lp-Space (M,k)) st Sq is Cauchy_sequence_by_Norm holds
Sq is convergent
let M be sigma_Measure of S; :: thesis: for k being geq_than_1 Real
for Sq being sequence of (Lp-Space (M,k)) st Sq is Cauchy_sequence_by_Norm holds
Sq is convergent
let k be geq_than_1 Real; :: thesis: for Sq being sequence of (Lp-Space (M,k)) st Sq is Cauchy_sequence_by_Norm holds
Sq is convergent
let Sq be sequence of (Lp-Space (M,k)); :: thesis: ( Sq is Cauchy_sequence_by_Norm implies Sq is convergent )
A1: 1 <= k by Def1;
assume A2: Sq is Cauchy_sequence_by_Norm ; :: thesis: Sq is convergent
consider Fsq being with_the_same_dom Functional_Sequence of X,REAL such that
A3: 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) ) ) by Th63;
Fsq . 0 in Lp_Functions (M,k) by A3;
then A4: ex D being Element of S st
( M . (D `) = 0 & dom (Fsq . 0) = D & Fsq . 0 is D -measurable ) by Th35;
then reconsider E = dom (Fsq . 0) as Element of S ;
consider N being increasing sequence of NAT such that
A5: for i, j being Nat st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i) by Th65, A2;
deffunc H₁( Nat) -> Element of bool [:X,REAL:] = Fsq . (N . $1);
consider F1 being Functional_Sequence of X,REAL such that
A6: for n being Nat holds F1 . n = H₁(n) from SEQFUNC:sch 1();
A7: for n being Nat holds
( dom (F1 . n) = E & F1 . n in Lp_Functions (M,k) & F1 . n is E -measurable & abs (F1 . n) in Lp_Functions (M,k) )

proof

let n be Nat; :: thesis: ( dom (F1 . n) = E & F1 . n in Lp_Functions (M,k) & F1 . n is E -measurable & abs (F1 . n) in Lp_Functions (M,k) )
A8: F1 . n = Fsq . (N . n) by A6;
hence A9: ( dom (F1 . n) = E & F1 . n in Lp_Functions (M,k) ) by A3, MESFUNC8:def 2; :: thesis: ( F1 . n is E -measurable & abs (F1 . n) in Lp_Functions (M,k) )
then consider F being PartFunc of X,REAL such that
Z1: ( F1 . n = F & ex ND being Element of S st
( M . (ND `) = 0 & dom F = ND & F is ND -measurable & (abs F) to_power k is_integrable_on M ) ) ;
consider ND being Element of S such that
Z2: ( M . (ND `) = 0 & dom F = ND & F is ND -measurable & (abs F) to_power k is_integrable_on M ) by Z1;
ND = E by Z1, Z2, A8, MESFUNC8:def 2;
hence F1 . n is E -measurable by Z1, Z2; :: thesis: abs (F1 . n) in Lp_Functions (M,k)
thus abs (F1 . n) in Lp_Functions (M,k) by A9, Th28; :: thesis: verum

end;

for n, m being Nat holds dom (F1 . n) = dom (F1 . m)

proof

let n, m be Nat; :: thesis: dom (F1 . n) = dom (F1 . m)
( dom (F1 . n) = E & dom (F1 . m) = E ) by A7;
hence dom (F1 . n) = dom (F1 . m) ; :: thesis: verum

end;

then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
deffunc H₂( Nat) -> Element of bool [:X,REAL:] = (F1 . ($1 + 1)) - (F1 . $1);
consider FMF being Functional_Sequence of X,REAL such that
A10: for n being Nat holds FMF . n = H₂(n) from SEQFUNC:sch 1();
A11: for n being Nat holds
( dom (FMF . n) = E & FMF . n in Lp_Functions (M,k) )

proof

let n be Nat; :: thesis: ( dom (FMF . n) = E & FMF . n in Lp_Functions (M,k) )
A12: ( dom (F1 . n) = E & dom (F1 . (n + 1)) = E ) by A7;
FMF . n = (F1 . (n + 1)) - (F1 . n) by A10;
then dom (FMF . n) = (dom (F1 . (n + 1))) /\ (dom (F1 . n)) by VALUED_1:12;
hence dom (FMF . n) = E by A12; :: thesis: FMF . n in Lp_Functions (M,k)
( Fsq . (N . (n + 1)) in Lp_Functions (M,k) & Fsq . (N . n) in Lp_Functions (M,k) ) by A3;
then ( F1 . (n + 1) in Lp_Functions (M,k) & F1 . n in Lp_Functions (M,k) ) by A6;
then (F1 . (n + 1)) - (F1 . n) in Lp_Functions (M,k) by Th27;
hence FMF . n in Lp_Functions (M,k) by A10; :: thesis: verum

end;

for n, m being Nat holds dom (FMF . n) = dom (FMF . m)

proof

let n, m be Nat; :: thesis: dom (FMF . n) = dom (FMF . m)
( dom (FMF . n) = E & dom (FMF . m) = E ) by A11;
hence dom (FMF . n) = dom (FMF . m) ; :: thesis: verum

end;

then reconsider FMF = FMF as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
set AbsFMF = abs FMF;
A13: for n being Nat holds
( (abs FMF) . n is nonnegative & dom ((abs FMF) . n) = E & abs ((abs FMF) . n) = (abs FMF) . n & (abs FMF) . n in Lp_Functions (M,k) & (abs FMF) . n is E -measurable )

proof

let n be Nat; :: thesis: ( (abs FMF) . n is nonnegative & dom ((abs FMF) . n) = E & abs ((abs FMF) . n) = (abs FMF) . n & (abs FMF) . n in Lp_Functions (M,k) & (abs FMF) . n is E -measurable )
A14: (abs FMF) . n = abs (FMF . n) by SEQFUNC:def 4;
hence (abs FMF) . n is nonnegative ; :: thesis: ( dom ((abs FMF) . n) = E & abs ((abs FMF) . n) = (abs FMF) . n & (abs FMF) . n in Lp_Functions (M,k) & (abs FMF) . n is E -measurable )
A15: ( dom (FMF . n) = E & FMF . n in Lp_Functions (M,k) ) by A11;
hence ( dom ((abs FMF) . n) = E & abs ((abs FMF) . n) = (abs FMF) . n ) by A14, VALUED_1:def 11; :: thesis: ( (abs FMF) . n in Lp_Functions (M,k) & (abs FMF) . n is E -measurable )
thus (abs FMF) . n in Lp_Functions (M,k) by A11, A14, Th28; :: thesis: (abs FMF) . n is E -measurable
then consider D being Element of S such that
Z1: ( M . (D `) = 0 & dom ((abs FMF) . n) = D & (abs FMF) . n is D -measurable ) by Th35;
D = E by Z1, A15, A14, VALUED_1:def 11;
hence (abs FMF) . n is E -measurable by Z1; :: thesis: verum

end;

reconsider AbsFMF = abs FMF as with_the_same_dom Functional_Sequence of X,REAL by Th69;
deffunc H₃( Nat) -> Element of bool [:X,REAL:] = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . $1);
consider G being Functional_Sequence of X,REAL such that
A16: for n being Nat holds G . n = H₃(n) from SEQFUNC:sch 1();
A17: for n being Nat holds
( dom (G . n) = E & G . n in Lp_Functions (M,k) & G . n is nonnegative & G . n is E -measurable & abs (G . n) = G . n )

proof

let n be Nat; :: thesis: ( dom (G . n) = E & G . n in Lp_Functions (M,k) & G . n is nonnegative & G . n is E -measurable & abs (G . n) = G . n )
A18: G . n = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . n) by A16;
then A19: dom (G . n) = (dom (abs (F1 . 0))) /\ (dom ((Partial_Sums AbsFMF) . n)) by VALUED_1:def 1
.= (dom (F1 . 0)) /\ (dom ((Partial_Sums AbsFMF) . n)) by VALUED_1:def 11
.= (dom (F1 . 0)) /\ (dom (AbsFMF . 0)) by MESFUN9C:11 ;
A20: ( (Partial_Sums AbsFMF) . n in Lp_Functions (M,k) & (Partial_Sums AbsFMF) . n is nonnegative & (Partial_Sums AbsFMF) . n is E -measurable ) by A13, Th66, Th67, MESFUN9C:16;
A21: dom (AbsFMF . 0) = E by A13;
A22: ( F1 . 0 in Lp_Functions (M,k) & dom (F1 . 0) = E & F1 . 0 is E -measurable ) by A7;
then ( abs (F1 . 0) in Lp_Functions (M,k) & abs (F1 . 0) is nonnegative & abs (F1 . 0) is E -measurable ) by Th28, MESFUNC6:48;
hence ( dom (G . n) = E & G . n in Lp_Functions (M,k) & G . n is nonnegative & G . n is E -measurable & abs (G . n) = G . n ) by A19, A22, A21, A18, A20, Th14, Th25, MESFUNC6:26, MESFUNC6:56; :: thesis: verum

end;

deffunc H₄( Nat) -> Element of bool [:X,REAL:] = (G . $1) to_power k;
consider Gp being Functional_Sequence of X,REAL such that
A23: for n being Nat holds Gp . n = H₄(n) from SEQFUNC:sch 1();
A24: for n being Nat holds
( (G . n) to_power k is nonnegative & (G . n) to_power k is E -measurable )

proof

let n be Nat; :: thesis: ( (G . n) to_power k is nonnegative & (G . n) to_power k is E -measurable )
A25: G . n is nonnegative by A17;
hence (G . n) to_power k is nonnegative ; :: thesis: (G . n) to_power k is E -measurable
( G . n is E -measurable & dom (G . n) = E ) by A17;
hence (G . n) to_power k is E -measurable by A25, MESFUN6C:29; :: thesis: verum

end;

reconsider ExtGp = R_EAL Gp as Functional_Sequence of X,ExtREAL ;
A26: for n being Nat holds
( dom (ExtGp . n) = E & ExtGp . n is E -measurable & ExtGp . n is nonnegative )

proof

let n be Nat; :: thesis: ( dom (ExtGp . n) = E & ExtGp . n is E -measurable & ExtGp . n is nonnegative )
ExtGp . n = R_EAL ((G . n) to_power k) by A23;
then dom (ExtGp . n) = dom (G . n) by MESFUN6C:def 4;
hence dom (ExtGp . n) = E by A17; :: thesis: ( ExtGp . n is E -measurable & ExtGp . n is nonnegative )
(G . n) to_power k is E -measurable by A24;
then R_EAL ((G . n) to_power k) is E -measurable ;
hence ExtGp . n is E -measurable by A23; :: thesis: ExtGp . n is nonnegative
(G . n) to_power k is nonnegative by A24;
hence ExtGp . n is nonnegative by A23; :: thesis: verum

end;

then A27: ( dom (ExtGp . 0) = E & ExtGp . 0 is nonnegative ) ;
for n, m being Nat holds dom (ExtGp . n) = dom (ExtGp . m)

proof

let n, m be Nat; :: thesis: dom (ExtGp . n) = dom (ExtGp . m)
( dom (ExtGp . n) = E & dom (ExtGp . m) = E ) by A26;
hence dom (ExtGp . n) = dom (ExtGp . m) ; :: thesis: verum

end;

then reconsider ExtGp = ExtGp as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
A28: for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(ExtGp . n) . x <= (ExtGp . m) . x

proof

let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in E holds
(ExtGp . n) . x <= (ExtGp . m) . x )
assume A29: n <= m ; :: thesis: for x being Element of X st x in E holds
(ExtGp . n) . x <= (ExtGp . m) . x
let x be Element of X; :: thesis: ( x in E implies (ExtGp . n) . x <= (ExtGp . m) . x )
assume A30: x in E ; :: thesis: (ExtGp . n) . x <= (ExtGp . m) . x
then A31: ( x in dom (G . n) & x in dom (G . m) ) by A17;
then ( x in dom ((G . n) to_power k) & x in dom ((G . m) to_power k) ) by MESFUN6C:def 4;
then ( ((G . n) . x) to_power k = ((G . n) to_power k) . x & ((G . m) . x) to_power k = ((G . m) to_power k) . x ) by MESFUN6C:def 4;
then A32: ( ((G . n) . x) to_power k = (ExtGp . n) . x & ((G . m) . x) to_power k = (ExtGp . m) . x ) by A23;
dom (AbsFMF . 0) = E by A13;
then ((Partial_Sums AbsFMF) . n) . x <= ((Partial_Sums AbsFMF) . m) . x by Th68, A29, A30, A13;
then A33: ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . n) . x) <= ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . m) . x) by XREAL_1:6;
( G . m = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . m) & G . n = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . n) ) by A16;
then A34: ( (G . m) . x = ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . m) . x) & (G . n) . x = ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . n) . x) ) by A31, VALUED_1:def 1;
G . n is nonnegative by A17;
then 0 <= (G . n) . x by MESFUNC6:51;
hence (ExtGp . n) . x <= (ExtGp . m) . x by A32, A33, A34, HOLDER_1:3; :: thesis: verum

end;

A35: for x being Element of X st x in E holds
ExtGp # x is non-decreasing

proof

let x be Element of X; :: thesis: ( x in E implies ExtGp # x is non-decreasing )
assume A36: x in E ; :: thesis: ExtGp # x is non-decreasing
for n, m being Nat st m <= n holds
(ExtGp # x) . m <= (ExtGp # x) . n

proof

let n, m be Nat; :: thesis: ( m <= n implies (ExtGp # x) . m <= (ExtGp # x) . n )
assume m <= n ; :: thesis: (ExtGp # x) . m <= (ExtGp # x) . n
then (ExtGp . m) . x <= (ExtGp . n) . x by A28, A36;
then (ExtGp # x) . m <= (ExtGp . n) . x by MESFUNC5:def 13;
hence (ExtGp # x) . m <= (ExtGp # x) . n by MESFUNC5:def 13; :: thesis: verum

end;

hence ExtGp # x is non-decreasing by RINFSUP2:7; :: thesis: verum

end;

A37: for x being Element of X st x in E holds
ExtGp # x is convergent

proof

let x be Element of X; :: thesis: ( x in E implies ExtGp # x is convergent )
assume x in E ; :: thesis: ExtGp # x is convergent
then ExtGp # x is non-decreasing by A35;
hence ExtGp # x is convergent by RINFSUP2:37; :: thesis: verum

end;

then consider I being ExtREAL_sequence such that
A38: ( ( for n being Nat holds I . n = Integral (M,(ExtGp . n)) ) & I is convergent & Integral (M,(lim ExtGp)) = lim I ) by A27, A26, A28, MESFUNC9:52;

now :: thesis: for y being object st y in rng I holds
y in REAL

let y be object ; :: thesis: ( y in rng I implies y in REAL )
assume y in rng I ; :: thesis: y in REAL
then consider x being Element of NAT such that
A39: y = I . x by FUNCT_2:113;
A40: y = Integral (M,(Gp . x)) by A39, A38;
G . x = abs (G . x) by A17;
then A41: Gp . x = (abs (G . x)) to_power k by A23;
G . x in Lp_Functions (M,k) by A17;
hence y in REAL by A40, A41, Th49; :: thesis: verum

end;

then rng I c= REAL ;
then reconsider Ir = I as sequence of REAL by FUNCT_2:6;
deffunc H₅( Nat) -> Element of ExtREAL = Integral (M,((AbsFMF . $1) to_power k));
A42: for x being Element of NAT holds H₅(x) is Element of REAL

proof

let x be Element of NAT ; :: thesis: H₅(x) is Element of REAL
AbsFMF . x in Lp_Functions (M,k) by A13;
then Integral (M,((abs (AbsFMF . x)) to_power k)) in REAL by Th49;
hence H₅(x) is Element of REAL by A13; :: thesis: verum

end;

consider KPAbsFMF being sequence of REAL such that
A43: for x being Element of NAT holds KPAbsFMF . x = H₅(x) from FUNCT_2:sch 9(A42);
deffunc H₆( Nat) -> object = (KPAbsFMF . $1) to_power (1 / k);
A44: for x being Element of NAT holds H₆(x) is Element of REAL by XREAL_0:def 1;
consider PAbsFMF being sequence of REAL such that
A45: for x being Element of NAT holds PAbsFMF . x = H₆(x) from FUNCT_2:sch 9(A44);
F1 . 0 in Lp_Functions (M,k) by A7;
then reconsider RF0 = Integral (M,((abs (F1 . 0)) to_power k)) as Element of REAL by Th49;
deffunc H₇( Nat) -> set = (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . $1);
A46: for x being Element of NAT holds H₇(x) is Element of REAL by XREAL_0:def 1;
consider QAbsFMF being sequence of REAL such that
A47: for x being Element of NAT holds QAbsFMF . x = H₇(x) from FUNCT_2:sch 9(A46);
A48: for n being Nat holds (Ir . n) to_power (1 / k) <= QAbsFMF . n

proof

defpred S₁[ Nat] means (Ir . $1) to_power (1 / k) <= QAbsFMF . $1;
A49: ( abs (F1 . 0) in Lp_Functions (M,k) & AbsFMF . 0 in Lp_Functions (M,k) ) by A13, A7;
G . 0 = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . 0) by A16;
then A50: G . 0 = (abs (F1 . 0)) + (AbsFMF . 0) by MESFUN9C:def 2;
Ir . 0 = Integral (M,(Gp . 0)) by A38;
then Ir . 0 = Integral (M,((G . 0) to_power k)) by A23;
then A51: Ir . 0 = Integral (M,((abs ((abs (F1 . 0)) + (AbsFMF . 0))) to_power k)) by A17, A50;
KPAbsFMF . 0 = Integral (M,((AbsFMF . 0) to_power k)) by A43;
then A52: KPAbsFMF . 0 = Integral (M,((abs (AbsFMF . 0)) to_power k)) by A13;
A53: RF0 = Integral (M,((abs (abs (F1 . 0))) to_power k)) ;
QAbsFMF . 0 = (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . 0) by A47;
then QAbsFMF . 0 = (RF0 to_power (1 / k)) + (PAbsFMF . 0) by SERIES_1:def 1;
then QAbsFMF . 0 = (RF0 to_power (1 / k)) + ((KPAbsFMF . 0) to_power (1 / k)) by A45;
then A54: S₁[ 0 ] by A1, A49, A51, A52, A53, Th61;

A55: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
A56: n in NAT by ORDINAL1:def 12;
assume S₁[n] ; :: thesis: S₁[n + 1]
then A57: ((Ir . n) to_power (1 / k)) + (PAbsFMF . (n + 1)) <= (QAbsFMF . n) + (PAbsFMF . (n + 1)) by XREAL_1:6;
G . (n + 1) = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . (n + 1)) by A16
.= (abs (F1 . 0)) + (((Partial_Sums AbsFMF) . n) + (AbsFMF . (n + 1))) by MESFUN9C:def 2
.= ((abs (F1 . 0)) + ((Partial_Sums AbsFMF) . n)) + (AbsFMF . (n + 1)) by RFUNCT_1:8 ;
then A58: G . (n + 1) = (G . n) + (AbsFMF . (n + 1)) by A16;
A59: ( AbsFMF . (n + 1) in Lp_Functions (M,k) & G . n in Lp_Functions (M,k) ) by A13, A17;
KPAbsFMF . (n + 1) = Integral (M,((AbsFMF . (n + 1)) to_power k)) by A43;
then A60: KPAbsFMF . (n + 1) = Integral (M,((abs (AbsFMF . (n + 1))) to_power k)) by A13;
A61: PAbsFMF . (n + 1) = (KPAbsFMF . (n + 1)) to_power (1 / k) by A45;
( Ir . n = Integral (M,(Gp . n)) & Ir . (n + 1) = Integral (M,(Gp . (n + 1))) ) by A38;
then ( Ir . n = Integral (M,((G . n) to_power k)) & Ir . (n + 1) = Integral (M,((G . (n + 1)) to_power k)) ) by A23;
then ( Ir . n = Integral (M,((abs (G . n)) to_power k)) & Ir . (n + 1) = Integral (M,((abs ((G . n) + (AbsFMF . (n + 1)))) to_power k)) ) by A58, A17;
then (Ir . (n + 1)) to_power (1 / k) <= ((Ir . n) to_power (1 / k)) + (PAbsFMF . (n + 1)) by A1, A59, A60, A61, Th61;
then A62: (Ir . (n + 1)) to_power (1 / k) <= (QAbsFMF . n) + (PAbsFMF . (n + 1)) by A57, XXREAL_0:2;
(QAbsFMF . n) + (PAbsFMF . (n + 1)) = ((RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . n)) + (PAbsFMF . (n + 1)) by A47, A56
.= (RF0 to_power (1 / k)) + (((Partial_Sums PAbsFMF) . n) + (PAbsFMF . (n + 1)))
.= (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . (n + 1)) by SERIES_1:def 1 ;
hence S₁[n + 1] by A62, A47; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A54, A55);
hence for n being Nat holds (Ir . n) to_power (1 / k) <= QAbsFMF . n ; :: thesis: verum

end;

A63: for n being Nat holds PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).||

proof

let n be Nat; :: thesis: PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).||
A64: n in NAT by ORDINAL1:def 12;
set m = N . n;
set m1 = N . (n + 1);
A65: ( F1 . (n + 1) = Fsq . (N . (n + 1)) & F1 . n = Fsq . (N . n) ) by A6;
AbsFMF . n = abs (FMF . n) by SEQFUNC:def 4;
then A66: AbsFMF . n = abs ((Fsq . (N . (n + 1))) - (Fsq . (N . n))) by A65, A10;
A67: ( Fsq . (N . (n + 1)) in Lp_Functions (M,k) & Fsq . (N . (n + 1)) in Sq . (N . (n + 1)) & Fsq . (N . n) in Lp_Functions (M,k) & Fsq . (N . n) in Sq . (N . n) ) by A3;
then (- 1) (#) (Fsq . (N . n)) in (- 1) * (Sq . (N . n)) by Th54;
then (Fsq . (N . (n + 1))) - (Fsq . (N . n)) in (Sq . (N . (n + 1))) + ((- 1) * (Sq . (N . n))) by Th54, A67;
then (Fsq . (N . (n + 1))) - (Fsq . (N . n)) in (Sq . (N . (n + 1))) - (Sq . (N . n)) by RLVECT_1:16;
then A68: ex r being Real st
( 0 <= r & r = Integral (M,((abs ((Fsq . (N . (n + 1))) - (Fsq . (N . n)))) to_power k)) & ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).|| = r to_power (1 / k) ) by Th53;
PAbsFMF . n = (KPAbsFMF . n) to_power (1 / k) by A45, A64;
hence PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).|| by A68, A66, A43, A64; :: thesis: verum

end;

1 / 2 < 1 ;
then |.(1 / 2).| < 1 by ABSVALUE:def 1;
then A69: ( (1 / 2) GeoSeq is summable & Sum ((1 / 2) GeoSeq) = 1 / (1 - (1 / 2)) ) by SERIES_1:24;
for n being Nat holds
( 0 <= PAbsFMF . n & PAbsFMF . n <= ((1 / 2) GeoSeq) . n )

proof

let n be Nat; :: thesis: ( 0 <= PAbsFMF . n & PAbsFMF . n <= ((1 / 2) GeoSeq) . n )
A70: PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).|| by A63;
hence 0 <= PAbsFMF . n ; :: thesis: PAbsFMF . n <= ((1 / 2) GeoSeq) . n
((1 / 2) GeoSeq) . n = (1 / 2) |^ n by PREPOWER:def 1
.= (1 / 2) to_power n by POWER:41 ;
then A71: ((1 / 2) GeoSeq) . n = 2 to_power (- n) by POWER:32;
N is Real_Sequence by FUNCT_2:7, NUMBERS:19;
then N . n < N . (n + 1) by SEQM_3:def 6;
hence PAbsFMF . n <= ((1 / 2) GeoSeq) . n by A5, A70, A71; :: thesis: verum

end;

then ( PAbsFMF is summable & Sum PAbsFMF <= Sum ((1 / 2) GeoSeq) ) by A69, SERIES_1:20;
then Partial_Sums PAbsFMF is convergent by SERIES_1:def 2;
then Partial_Sums PAbsFMF is bounded ;
then consider Br being Real such that
A72: for n being Nat holds (Partial_Sums PAbsFMF) . n < Br by SEQ_2:def 3;
for n being Nat holds Ir . n < ((RF0 to_power (1 / k)) + Br) to_power k

proof

let n be Nat; :: thesis: Ir . n < ((RF0 to_power (1 / k)) + Br) to_power k
A73: n in NAT by ORDINAL1:def 12;
(Ir . n) to_power (1 / k) <= QAbsFMF . n by A48;
then A74: (Ir . n) to_power (1 / k) <= (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . n) by A47, A73;
(RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . n) < (RF0 to_power (1 / k)) + Br by A72, XREAL_1:8;
then A75: (Ir . n) to_power (1 / k) < (RF0 to_power (1 / k)) + Br by A74, XXREAL_0:2;
Ir . n = Integral (M,(Gp . n)) by A38;
then Ir . n = Integral (M,((G . n) to_power k)) by A23;
then A76: Ir . n = Integral (M,((abs (G . n)) to_power k)) by A17;
A77: G . n in Lp_Functions (M,k) by A17;
then 0 <= (Ir . n) to_power (1 / k) by Th49, A76, Th4;
then ((Ir . n) to_power (1 / k)) to_power k < ((RF0 to_power (1 / k)) + Br) to_power k by A75, Th3;
then (Ir . n) to_power ((1 / k) * k) < ((RF0 to_power (1 / k)) + Br) to_power k by A77, Th49, A76, HOLDER_1:2;
then (Ir . n) to_power 1 < ((RF0 to_power (1 / k)) + Br) to_power k by XCMPLX_1:106;
hence Ir . n < ((RF0 to_power (1 / k)) + Br) to_power k by POWER:25; :: thesis: verum

end;

then A78: Ir is bounded_above by SEQ_2:def 3;
for n, m being Nat st n <= m holds
Ir . n <= Ir . m

proof

let n, m be Nat; :: thesis: ( n <= m implies Ir . n <= Ir . m )
assume n <= m ; :: thesis: Ir . n <= Ir . m
then A79: for x being Element of X st x in E holds
(ExtGp . n) . x <= (ExtGp . m) . x by A28;
A80: ( ExtGp . n is E -measurable & ExtGp . m is E -measurable & ExtGp . n is nonnegative & ExtGp . m is nonnegative ) by A26;
A81: ( dom (ExtGp . n) = E & dom (ExtGp . m) = E ) by A26;
then A82: ( (ExtGp . n) | E = ExtGp . n & (ExtGp . m) | E = ExtGp . m ) by RELAT_1:68;
( I . n = Integral (M,(ExtGp . n)) & I . m = Integral (M,(ExtGp . m)) ) by A38;
hence Ir . n <= Ir . m by A79, A81, A80, A82, MESFUNC9:15; :: thesis: verum

end;

then Ir is non-decreasing by SEQM_3:6;
then A83: ( I is convergent_to_finite_number & lim I = lim Ir ) by A78, RINFSUP2:14;
reconsider LExtGp = lim ExtGp as PartFunc of X,ExtREAL ;
A84: ( E = dom LExtGp & LExtGp is E -measurable ) by A26, A27, A37, MESFUNC8:25, MESFUNC8:def 9;
A85: for x being object st x in dom LExtGp holds
0 <= LExtGp . x

proof

let x be object ; :: thesis: ( x in dom LExtGp implies 0 <= LExtGp . x )
assume A86: x in dom LExtGp ; :: thesis: 0 <= LExtGp . x
then reconsider x1 = x as Element of X ;
A87: x1 in E by A27, A86, MESFUNC8:def 9;

now :: thesis: for k1 being Nat holds 0 <= (ExtGp # x1) . k1

let k1 be Nat; :: thesis: 0 <= (ExtGp # x1) . k1
reconsider k = k1 as Nat ;
ExtGp # x1 is non-decreasing by A35, A87;
then A88: (ExtGp # x1) . 0 <= (ExtGp # x1) . k by RINFSUP2:7;
0 <= (ExtGp . 0) . x1 by A27, SUPINF_2:39;
hence 0 <= (ExtGp # x1) . k1 by A88, MESFUNC5:def 13; :: thesis: verum

end;

then 0 <= lim (ExtGp # x1) by A87, A37, MESFUNC9:10;
hence 0 <= LExtGp . x by A86, MESFUNC8:def 9; :: thesis: verum

end;

A89: eq_dom (LExtGp,+infty) = E /\ (eq_dom (LExtGp,+infty)) by A84, RELAT_1:132, XBOOLE_1:28;
then reconsider EE = eq_dom (LExtGp,+infty) as Element of S by A84, MESFUNC1:33;
reconsider E0 = E \ EE as Element of S ;
E0 ` = (X \ E) \/ (X /\ EE) by XBOOLE_1:52;
then A90: E0 ` = (E `) \/ EE by XBOOLE_1:28;
M . EE = 0 by A38, A83, A84, A85, A89, MESFUNC9:13, SUPINF_2:52;
then A91: EE is measure_zero of M by MEASURE1:def 7;
E ` is Element of S by MEASURE1:34;
then E ` is measure_zero of M by A4, MEASURE1:def 7;
then E0 ` is measure_zero of M by A90, A91, MEASURE1:37;
then A92: M . (E0 `) = 0 by MEASURE1:def 7;
A93: for x being Element of X st x in E0 holds
LExtGp . x in REAL

proof

let x be Element of X; :: thesis: ( x in E0 implies LExtGp . x in REAL )
assume x in E0 ; :: thesis: LExtGp . x in REAL
then ( x in E & not x in EE ) by XBOOLE_0:def 5;
then ( LExtGp . x <> +infty & 0 <= LExtGp . x ) by A84, A85, MESFUNC1:def 15;
hence LExtGp . x in REAL by XXREAL_0:14; :: thesis: verum

end;

A94: for x being Element of X st x in E0 holds
( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) )

proof

let x be Element of X; :: thesis: ( x in E0 implies ( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) ) )
assume A95: x in E0 ; :: thesis: ( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) )
then A96: x in E by XBOOLE_0:def 5;
then LExtGp . x = lim (ExtGp # x) by A84, MESFUNC8:def 9;
then A97: lim (ExtGp # x) in REAL by A93, A95;
ExtGp # x is convergent by A37, A96;
then A98: ex g being Real st
( lim (ExtGp # x) = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((ExtGp # x) . m) - (lim (ExtGp # x))).| < p ) & ExtGp # x is convergent_to_finite_number ) by A97, MESFUNC5:def 12;
ExtGp # x = Gp # x by MESFUN7C:1;
hence ( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) ) by A98, RINFSUP2:15; :: thesis: verum

end;

A99: for x being Element of X st x in E0 holds
for n being Nat holds (Gp # x) . n = ((G # x) . n) to_power k

proof

let x be Element of X; :: thesis: ( x in E0 implies for n being Nat holds (Gp # x) . n = ((G # x) . n) to_power k )
assume A100: x in E0 ; :: thesis: for n being Nat holds (Gp # x) . n = ((G # x) . n) to_power k

hereby :: thesis: verum

let n be Nat; :: thesis: (Gp # x) . n = ((G # x) . n) to_power k
x in E by A100, XBOOLE_0:def 5;
then x in dom (G . n) by A17;
then A101: x in dom ((G . n) to_power k) by MESFUN6C:def 4;
(Gp # x) . n = (Gp . n) . x by SEQFUNC:def 10
.= ((G . n) to_power k) . x by A23
.= ((G . n) . x) to_power k by A101, MESFUN6C:def 4 ;
hence (Gp # x) . n = ((G # x) . n) to_power k by SEQFUNC:def 10; :: thesis: verum

end;

end;

A102: for x being Element of X st x in E0 holds
(Partial_Sums AbsFMF) # x is convergent

proof

let x be Element of X; :: thesis: ( x in E0 implies (Partial_Sums AbsFMF) # x is convergent )
assume A103: x in E0 ; :: thesis: (Partial_Sums AbsFMF) # x is convergent
then A104: Gp # x is convergent by A94;

A105: now :: thesis: for n being Nat holds 0 <= (G # x) . n

let n be Nat; :: thesis: 0 <= (G # x) . n
G . n is nonnegative by A17;
then 0 <= (G . n) . x by MESFUNC6:51;
hence 0 <= (G # x) . n by SEQFUNC:def 10; :: thesis: verum

end;

for n being Nat holds (Gp # x) . n = ((G # x) . n) to_power k by A103, A99;
then A106: G # x is convergent by A104, A105, Th9;

now :: thesis: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
|.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s )
assume 0 < s ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s
then consider n being Nat such that
A107: for m being Nat st n <= m holds
|.(((G # x) . m) - ((G # x) . n)).| < s by A106, SEQ_4:41;

now :: thesis: for m being Nat st n <= m holds
|.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s

let m be Nat; :: thesis: ( n <= m implies |.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s )
assume A108: n <= m ; :: thesis: |.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s
x in E by A103, XBOOLE_0:def 5;
then A109: ( x in dom (G . n) & x in dom (G . m) ) by A17;
( G . m = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . m) & G . n = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . n) ) by A16;
then ( (G . m) . x = ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . m) . x) & (G . n) . x = ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . n) . x) ) by A109, VALUED_1:def 1;
then ( (G # x) . m = ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . m) . x) & (G # x) . n = ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . n) . x) ) by SEQFUNC:def 10;
then A110: ((G # x) . m) - ((G # x) . n) = (((Partial_Sums AbsFMF) . m) . x) - (((Partial_Sums AbsFMF) . n) . x) ;
( ((Partial_Sums AbsFMF) # x) . m = ((Partial_Sums AbsFMF) . m) . x & ((Partial_Sums AbsFMF) # x) . n = ((Partial_Sums AbsFMF) . n) . x ) by SEQFUNC:def 10;
hence |.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s by A107, A108, A110; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s ; :: thesis: verum

end;

hence (Partial_Sums AbsFMF) # x is convergent by SEQ_4:41; :: thesis: verum

end;

A111: for x being Element of X st x in E0 holds
Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x

proof

let x be Element of X; :: thesis: ( x in E0 implies Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x )
assume x in E0 ; :: thesis: Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x
then A112: x in E by XBOOLE_0:def 5;
defpred S₁[ Nat] means (Partial_Sums (abs (FMF # x))) . $1 = ((Partial_Sums AbsFMF) # x) . $1;
(Partial_Sums (abs (FMF # x))) . 0 = (abs (FMF # x)) . 0 by SERIES_1:def 1
.= |.((FMF # x) . 0).| by VALUED_1:18
.= |.((FMF . 0) . x).| by SEQFUNC:def 10
.= (abs (FMF . 0)) . x by VALUED_1:18
.= (AbsFMF . 0) . x by SEQFUNC:def 4
.= ((Partial_Sums AbsFMF) . 0) . x by MESFUN9C:def 2
.= ((Partial_Sums AbsFMF) # x) . 0 by SEQFUNC:def 10 ;
then A113: S₁[ 0 ] ;

A114: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A115: S₁[n] ; :: thesis: S₁[n + 1]
A116: (Partial_Sums AbsFMF) . (n + 1) = ((Partial_Sums AbsFMF) . n) + (AbsFMF . (n + 1)) by MESFUN9C:def 2;
dom (AbsFMF . 0) = E by A13;
then A117: x in dom ((Partial_Sums AbsFMF) . (n + 1)) by A112, MESFUN9C:11;
A118: (abs (FMF # x)) . (n + 1) = |.((FMF # x) . (n + 1)).| by VALUED_1:18
.= |.((FMF . (n + 1)) . x).| by SEQFUNC:def 10
.= (abs (FMF . (n + 1))) . x by VALUED_1:18
.= (AbsFMF . (n + 1)) . x by SEQFUNC:def 4 ;
(Partial_Sums (abs (FMF # x))) . (n + 1) = ((Partial_Sums (abs (FMF # x))) . n) + ((abs (FMF # x)) . (n + 1)) by SERIES_1:def 1
.= (((Partial_Sums AbsFMF) . n) . x) + ((AbsFMF . (n + 1)) . x) by A115, A118, SEQFUNC:def 10
.= ((Partial_Sums AbsFMF) . (n + 1)) . x by A116, A117, VALUED_1:def 1
.= ((Partial_Sums AbsFMF) # x) . (n + 1) by SEQFUNC:def 10 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A113, A114);
then for n being Element of NAT holds S₁[n] ;
hence Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x by FUNCT_2:63; :: thesis: verum

end;

A119: for x being Element of X st x in E0 holds
for n being Nat holds (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)

proof

let x be Element of X; :: thesis: ( x in E0 implies for n being Nat holds (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n) )
assume x in E0 ; :: thesis: for n being Nat holds (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)
then A120: x in E by XBOOLE_0:def 5;
defpred S₁[ Nat] means (F1 # x) . ($1 + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . $1);
dom (FMF . 0) = E by A11;
then A121: x in dom ((F1 . (0 + 1)) - (F1 . 0)) by A10, A120;
(Partial_Sums (FMF # x)) . 0 = (FMF # x) . 0 by SERIES_1:def 1
.= (FMF . 0) . x by SEQFUNC:def 10
.= ((F1 . (0 + 1)) - (F1 . 0)) . x by A10 ;
then A122: (Partial_Sums (FMF # x)) . 0 = ((F1 . (0 + 1)) . x) - ((F1 . 0) . x) by A121, VALUED_1:13;
((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . 0) = ((F1 . 0) . x) + ((Partial_Sums (FMF # x)) . 0) by SEQFUNC:def 10;
then A123: S₁[ 0 ] by A122, SEQFUNC:def 10;

A124: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A125: S₁[n] ; :: thesis: S₁[n + 1]
dom (FMF . (n + 1)) = E by A11;
then A126: x in dom ((F1 . ((n + 1) + 1)) - (F1 . (n + 1))) by A10, A120;
(FMF # x) . (n + 1) = (FMF . (n + 1)) . x by SEQFUNC:def 10
.= ((F1 . ((n + 1) + 1)) - (F1 . (n + 1))) . x by A10 ;
then A127: (FMF # x) . (n + 1) = ((F1 . ((n + 1) + 1)) . x) - ((F1 . (n + 1)) . x) by A126, VALUED_1:13;
((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . (n + 1)) = ((F1 # x) . 0) + (((Partial_Sums (FMF # x)) . n) + ((FMF # x) . (n + 1))) by SERIES_1:def 1
.= (((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)) + ((FMF # x) . (n + 1))
.= ((F1 . (n + 1)) . x) + ((FMF # x) . (n + 1)) by A125, SEQFUNC:def 10 ;
hence S₁[n + 1] by A127, SEQFUNC:def 10; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A123, A124);
hence for n being Nat holds (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n) ; :: thesis: verum

end;

A128: for x being Element of X st x in E0 holds
F1 # x is convergent

proof

let x be Element of X; :: thesis: ( x in E0 implies F1 # x is convergent )
assume A129: x in E0 ; :: thesis: F1 # x is convergent
then Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x by A111;
then Partial_Sums (abs (FMF # x)) is convergent by A129, A102;
then abs (FMF # x) is summable by SERIES_1:def 2;
then FMF # x is absolutely_summable by SERIES_1:def 4;
then FMF # x is summable ;
then A130: Partial_Sums (FMF # x) is convergent by SERIES_1:def 2;

now :: thesis: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((F1 # x) . m) - ((F1 # x) . n)).| < s

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
|.(((F1 # x) . m) - ((F1 # x) . n)).| < s )
assume 0 < s ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((F1 # x) . m) - ((F1 # x) . n)).| < s
then consider n being Nat such that
A131: for m being Nat st n <= m holds
|.(((Partial_Sums (FMF # x)) . m) - ((Partial_Sums (FMF # x)) . n)).| < s by A130, SEQ_4:41;
set n1 = n + 1;

now :: thesis: for m1 being Nat st n + 1 <= m1 holds
|.(((F1 # x) . m1) - ((F1 # x) . (n + 1))).| < s

let m1 be Nat; :: thesis: ( n + 1 <= m1 implies |.(((F1 # x) . m1) - ((F1 # x) . (n + 1))).| < s )
assume A132: n + 1 <= m1 ; :: thesis: |.(((F1 # x) . m1) - ((F1 # x) . (n + 1))).| < s
1 <= n + 1 by NAT_1:11;
then reconsider m = m1 - 1 as Nat by A132, NAT_1:21, XXREAL_0:2;
(n + 1) - 1 <= m1 - 1 by A132, XREAL_1:9;
then A133: |.(((Partial_Sums (FMF # x)) . m) - ((Partial_Sums (FMF # x)) . n)).| < s by A131;
m1 = m + 1 ;
then ( (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n) & (F1 # x) . m1 = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . m) ) by A119, A129;
hence |.(((F1 # x) . m1) - ((F1 # x) . (n + 1))).| < s by A133; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.(((F1 # x) . m) - ((F1 # x) . n)).| < s ; :: thesis: verum

end;

hence F1 # x is convergent by SEQ_4:41; :: thesis: verum

end;

set F2 = F1 || E0;
A134: for x being Element of X st x in E0 holds
(F1 || E0) # x is convergent

proof

let x be Element of X; :: thesis: ( x in E0 implies (F1 || E0) # x is convergent )
assume A135: x in E0 ; :: thesis: (F1 || E0) # x is convergent
then F1 # x is convergent by A128;
hence (F1 || E0) # x is convergent by A135, MESFUN9C:1; :: thesis: verum

end;

A136: for x being Element of X st x in E0 holds
(F1 || E0) # x = F1 # x

proof

let x be Element of X; :: thesis: ( x in E0 implies (F1 || E0) # x = F1 # x )
assume A137: x in E0 ; :: thesis: (F1 || E0) # x = F1 # x

now :: thesis: for n being Element of NAT holds ((F1 || E0) # x) . n = (F1 # x) . n

let n be Element of NAT ; :: thesis: ((F1 || E0) # x) . n = (F1 # x) . n
((F1 || E0) # x) . n = ((F1 || E0) . n) . x by SEQFUNC:def 10
.= ((F1 . n) | E0) . x by MESFUN9C:def 1
.= (F1 . n) . x by A137, FUNCT_1:49 ;
hence ((F1 || E0) # x) . n = (F1 # x) . n by SEQFUNC:def 10; :: thesis: verum

end;

hence (F1 || E0) # x = F1 # x by FUNCT_2:63; :: thesis: verum

end;

A138: for n being Nat holds
( dom ((F1 || E0) . n) = E0 & (F1 || E0) . n is E0 -measurable )

proof

let n be Nat; :: thesis: ( dom ((F1 || E0) . n) = E0 & (F1 || E0) . n is E0 -measurable )
A139: dom (F1 . 0) = E by A7;
dom ((F1 || E0) . n) = dom ((F1 . n) | E0) by MESFUN9C:def 1;
then dom ((F1 || E0) . n) = (dom (F1 . n)) /\ E0 by RELAT_1:61;
then dom ((F1 || E0) . n) = E /\ E0 by A7;
hence dom ((F1 || E0) . n) = E0 by XBOOLE_1:28, XBOOLE_1:36; :: thesis: (F1 || E0) . n is E0 -measurable
for m being Nat holds F1 . m is E0 -measurable

proof

let m be Nat; :: thesis: F1 . m is E0 -measurable
F1 . m is E -measurable by A7;
hence F1 . m is E0 -measurable by MESFUNC6:16, XBOOLE_1:36; :: thesis: verum

end;

hence (F1 || E0) . n is E0 -measurable by A139, MESFUN9C:4, XBOOLE_1:36; :: thesis: verum

end;

reconsider F2 = F1 || E0 as with_the_same_dom Functional_Sequence of X,REAL by MESFUN9C:2;
A140: for n being Nat holds
( F2 . n in Lp_Functions (M,k) & F2 . n in Sq . (N . n) )

proof

let n1 be Nat; :: thesis: ( F2 . n1 in Lp_Functions (M,k) & F2 . n1 in Sq . (N . n1) )
F2 . n1 = (F1 . n1) | E0 by MESFUN9C:def 1;
then abs (F2 . n1) = (abs (F1 . n1)) | E0 by Th13;
then A141: ((abs (F1 . n1)) to_power k) | E0 = (abs (F2 . n1)) to_power k by Th20;
A142: ( F2 . n1 is E0 -measurable & dom (F2 . n1) = E0 ) by A138;
F1 . n1 in Lp_Functions (M,k) by A7;
then ex FMF being PartFunc of X,REAL st
( F1 . n1 = 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 (abs (F2 . n1)) to_power k is_integrable_on M by A141, MESFUNC6:91;
hence A143: F2 . n1 in Lp_Functions (M,k) by A142, A92; :: thesis: F2 . n1 in Sq . (N . n1)
reconsider n = n1 as Nat ;
set m = N . n;
F1 . n = Fsq . (N . n) by A6;
then A144: ( F1 . n in Sq . (N . n) & Sq . (N . n) = a.e-eq-class_Lp ((F1 . n),M,k) ) by A3;
reconsider EB = E0 ` as Element of S by MEASURE1:34;
(F2 . n) | (EB `) = F2 . n by A142, RELAT_1:68;
then (F2 . n) | (EB `) = (F1 . n) | (EB `) by MESFUN9C:def 1;
then F2 . n a.e.= F1 . n,M by A92;
hence F2 . n1 in Sq . (N . n1) by A143, A144, Th36; :: thesis: verum

end;

A145: dom (lim F2) = dom (F2 . 0) by MESFUNC8:def 9;
then A146: dom (lim F2) = E0 by A138;
A147: for x being Element of X st x in E0 holds
(lim F2) . x = lim (F2 # x)

proof

let x be Element of X; :: thesis: ( x in E0 implies (lim F2) . x = lim (F2 # x) )
assume x in E0 ; :: thesis: (lim F2) . x = lim (F2 # x)
then ( (lim F2) . x = lim (R_EAL (F2 # x)) & F2 # x is convergent ) by A146, A134, MESFUN7C:14;
hence (lim F2) . x = lim (F2 # x) by RINFSUP2:14; :: thesis: verum

end;

now :: thesis: for y being object st y in rng (lim F2) holds
y in REAL

let y be object ; :: thesis: ( y in rng (lim F2) implies y in REAL )
assume y in rng (lim F2) ; :: thesis: y in REAL
then consider x being Element of X such that
A148: ( x in dom (lim F2) & y = (lim F2) . x ) by PARTFUN1:3;
y = lim (F2 # x) by A148, A146, A147;
hence y in REAL by XREAL_0:def 1; :: thesis: verum

end;

then rng (lim F2) c= REAL ;
then reconsider F = lim F2 as PartFunc of X,REAL by A145, RELSET_1:4;
A149: dom (LExtGp | E0) = E /\ E0 by A84, RELAT_1:61;
then A150: dom (LExtGp | E0) = E0 by XBOOLE_1:28, XBOOLE_1:36;

now :: thesis: for y being object st y in rng (LExtGp | E0) holds
y in REAL

let y be object ; :: thesis: ( y in rng (LExtGp | E0) implies y in REAL )
assume y in rng (LExtGp | E0) ; :: thesis: y in REAL
then consider x being Element of X such that
A151: ( x in dom (LExtGp | E0) & y = (LExtGp | E0) . x ) by PARTFUN1:3;
y = LExtGp . x by A150, A151, FUNCT_1:49;
hence y in REAL by A150, A151, A93; :: thesis: verum

end;

then rng (LExtGp | E0) c= REAL ;
then reconsider gp = LExtGp | E0 as PartFunc of X,REAL by A149, RELSET_1:4;
A152: for x being Element of X st x in E0 holds
gp . x = lim (Gp # x)

proof

let x be Element of X; :: thesis: ( x in E0 implies gp . x = lim (Gp # x) )
assume A153: x in E0 ; :: thesis: gp . x = lim (Gp # x)
then x in dom LExtGp by A84, XBOOLE_0:def 5;
then LExtGp . x = lim (ExtGp # x) by MESFUNC8:def 9;
then gp . x = lim (ExtGp # x) by A153, FUNCT_1:49;
hence gp . x = lim (Gp # x) by A94, A153; :: thesis: verum

end;

A154: LExtGp is nonnegative by A85, SUPINF_2:52;
Integral (M,LExtGp) in REAL by A83, A38, XREAL_0:def 1;
then LExtGp is_integrable_on M by A154, A84, Th2;
then R_EAL gp is_integrable_on M by MESFUNC5:97;
then A155: gp is_integrable_on M ;
A156: dom (F2 . 0) = E0 by A138;
then A157: dom F = E0 by MESFUNC8:def 9;
then A158: E0 = dom (abs F) by VALUED_1:def 11;
then A159: E0 = dom ((abs F) to_power k) by MESFUN6C:def 4;
A160: for x being Element of X
for n being Nat st x in E0 holds
|.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| <= (G # x) . n

proof

let x be Element of X; :: thesis: for n being Nat st x in E0 holds
|.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| <= (G # x) . n
let n be Nat; :: thesis: ( x in E0 implies |.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| <= (G # x) . n )
assume A161: x in E0 ; :: thesis: |.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| <= (G # x) . n
then x in E by XBOOLE_0:def 5;
then A162: x in dom (G . n) by A17;
G . n = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . n) by A16;
then (G . n) . x = ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . n) . x) by A162, VALUED_1:def 1;
then A163: (G . n) . x = |.((F1 . 0) . x).| + (((Partial_Sums AbsFMF) . n) . x) by VALUED_1:18;
(G # x) . n = (G . n) . x by SEQFUNC:def 10
.= |.((F1 . 0) . x).| + (((Partial_Sums AbsFMF) # x) . n) by A163, SEQFUNC:def 10
.= |.((F1 # x) . 0).| + (((Partial_Sums AbsFMF) # x) . n) by SEQFUNC:def 10 ;
then A164: (G # x) . n = |.((F1 # x) . 0).| + ((Partial_Sums (abs (FMF # x))) . n) by A111, A161;
|.((Partial_Sums (FMF # x)) . n).| <= (Partial_Sums (abs (FMF # x))) . n by Lm1;
hence |.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| <= (G # x) . n by A164, XREAL_1:6; :: thesis: verum

end;

A165: for x being Element of X
for n being Nat st x in E0 holds
|.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| to_power k <= (Gp # x) . n

proof

let x be Element of X; :: thesis: for n being Nat st x in E0 holds
|.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| to_power k <= (Gp # x) . n
let n be Nat; :: thesis: ( x in E0 implies |.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| to_power k <= (Gp # x) . n )
assume A166: x in E0 ; :: thesis: |.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| to_power k <= (Gp # x) . n
then A167: (Gp # x) . n = ((G # x) . n) to_power k by A99;
A168: |.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| <= (G # x) . n by A160, A166;
|.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| <= |.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| by COMPLEX1:56;
then A169: |.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| <= (G # x) . n by A168, XXREAL_0:2;
0 <= |.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| by COMPLEX1:46;
hence |.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| to_power k <= (Gp # x) . n by A167, A169, HOLDER_1:3; :: thesis: verum

end;

A170: for x being Element of X
for n being Nat st x in E0 holds
|.((F2 # x) . n).| to_power k <= (Gp # x) . n

proof

let x be Element of X; :: thesis: for n being Nat st x in E0 holds
|.((F2 # x) . n).| to_power k <= (Gp # x) . n
let n be Nat; :: thesis: ( x in E0 implies |.((F2 # x) . n).| to_power k <= (Gp # x) . n )
assume A171: x in E0 ; :: thesis: |.((F2 # x) . n).| to_power k <= (Gp # x) . n
then A172: F1 # x = F2 # x by A136;

per cases ( n = 0 or n <> 0 ) ;

suppose A173: n = 0 ; :: thesis: |.((F2 # x) . n).| to_power k <= (Gp # x) . n

A174: (Gp # x) . n = ((G # x) . n) to_power k by A171, A99;
A175: |.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| <= (G # x) . n by A160, A171;
0 <= |.((Partial_Sums (FMF # x)) . n).| by COMPLEX1:46;
then 0 + |.((F1 # x) . 0).| <= |.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| by XREAL_1:6;
then A176: |.((F1 # x) . 0).| <= (G # x) . n by A175, XXREAL_0:2;
0 <= |.((F1 # x) . 0).| by COMPLEX1:46;
hence |.((F2 # x) . n).| to_power k <= (Gp # x) . n by A172, A173, A174, A176, HOLDER_1:3; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: |.((F2 # x) . n).| to_power k <= (Gp # x) . n

then consider m being Nat such that
A177: n = m + 1 by NAT_1:6;
reconsider m = m as Nat ;
(F1 # x) . (m + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . m) by A119, A171;
then A178: |.((F1 # x) . (m + 1)).| to_power k <= (Gp # x) . m by A165, A171;
x in E by A171, XBOOLE_0:def 5;
then A179: ExtGp # x is non-decreasing by A35;
A180: (ExtGp # x) . m <= (ExtGp # x) . (m + 1) by A179;
ExtGp # x = Gp # x by MESFUN7C:1;
hence |.((F2 # x) . n).| to_power k <= (Gp # x) . n by A172, A177, A178, A180, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A181: for x being Element of X st x in E0 holds
|.(((abs F) to_power k) . x).| <= gp . x

proof

let x be Element of X; :: thesis: ( x in E0 implies |.(((abs F) to_power k) . x).| <= gp . x )
assume A182: x in E0 ; :: thesis: |.(((abs F) to_power k) . x).| <= gp . x
then A183: Gp # x is convergent by A94;
deffunc H₈( set ) -> object = ((abs (F2 # x)) . $1) to_power k;
consider s being Real_Sequence such that
A184: for n being Nat holds s . n = H₈(n) from SEQ_1:sch 1();
A185: gp . x = lim (Gp # x) by A152, A182;
A186: ((abs F) to_power k) . x = ((abs F) . x) to_power k by A159, A182, MESFUN6C:def 4
.= |.(F . x).| to_power k by A158, A182, VALUED_1:def 11
.= |.(lim (F2 # x)).| to_power k by A182, A147
.= (lim (abs (F2 # x))) to_power k by A134, A182, SEQ_4:14 ;

A187: now :: thesis: for n being Nat holds 0 <= (abs (F2 # x)) . n

let n be Nat; :: thesis: 0 <= (abs (F2 # x)) . n
0 <= |.((F2 # x) . n).| by COMPLEX1:46;
hence 0 <= (abs (F2 # x)) . n by VALUED_1:18; :: thesis: verum

end;

abs (F2 # x) is convergent by A182, A134, SEQ_4:13;
then A188: ( s is convergent & (lim (abs (F2 # x))) to_power k = lim s ) by A187, A184, HOLDER_1:10;

now :: thesis: for n being Nat holds s . n <= (Gp # x) . n

let n be Nat; :: thesis: s . n <= (Gp # x) . n
|.((F2 # x) . n).| to_power k <= (Gp # x) . n by A170, A182;
then ((abs (F2 # x)) . n) to_power k <= (Gp # x) . n by VALUED_1:18;
hence s . n <= (Gp # x) . n by A184; :: thesis: verum

end;

then A189: ((abs F) to_power k) . x <= gp . x by A188, A185, A186, A183, SEQ_2:18;
0 <= ((abs F) to_power k) . x by MESFUNC6:51;
hence |.(((abs F) to_power k) . x).| <= gp . x by A189, ABSVALUE:def 1; :: thesis: verum

end;

R_EAL F is E0 -measurable by A138, A156, A134, MESFUN7C:21;
then A190: F is E0 -measurable ;
then A191: abs F is E0 -measurable by A157, MESFUNC6:48;
dom (abs F) = E0 by A157, VALUED_1:def 11;
then (abs F) to_power k is E0 -measurable by A191, MESFUN6C:29;
then (abs F) to_power k is_integrable_on M by A150, A155, A159, A181, MESFUNC6:96;
then A192: F in Lp_Functions (M,k) by A92, A157, A190;
A193: for x being Element of X
for n, m being Nat st x in E0 & m <= n holds
|.(((F1 # x) . n) - ((F1 # x) . m)).| to_power k <= (Gp # x) . n

proof

let x be Element of X; :: thesis: for n, m being Nat st x in E0 & m <= n holds
|.(((F1 # x) . n) - ((F1 # x) . m)).| to_power k <= (Gp # x) . n
let n1, m1 be Nat; :: thesis: ( x in E0 & m1 <= n1 implies |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 )
assume A194: ( x in E0 & m1 <= n1 ) ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

now :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

per cases ( m1 = 0 or m1 <> 0 ) ;

suppose A195: m1 = 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

now :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

per cases ( n1 = 0 or n1 <> 0 ) ;

suppose A196: n1 = 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

(G . n1) to_power k is nonnegative by A24;
then Gp . n1 is nonnegative by A23;
then 0 <= (Gp . n1) . x by MESFUNC6:51;
then 0 <= (Gp # x) . n1 by SEQFUNC:def 10;
hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 by A195, A196, COMPLEX1:44, POWER:def 2; :: thesis: verum

end;

suppose n1 <> 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

then consider n being Nat such that
A197: n1 = n + 1 by NAT_1:6;
reconsider n = n as Nat ;
A198: (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n) by A194, A119;
A199: |.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| <= (G # x) . n by A160, A194;
0 <= |.((F1 # x) . 0).| by COMPLEX1:46;
then |.((Partial_Sums (FMF # x)) . n).| + 0 <= |.((F1 # x) . 0).| + |.((Partial_Sums (FMF # x)) . n).| by XREAL_1:6;
then A200: |.((Partial_Sums (FMF # x)) . n).| <= (G # x) . n by A199, XXREAL_0:2;
0 <= |.((Partial_Sums (FMF # x)) . n).| by COMPLEX1:46;
then A201: |.((Partial_Sums (FMF # x)) . n).| to_power k <= ((G # x) . n) to_power k by A200, HOLDER_1:3;
A202: (Gp # x) . n = ((G # x) . n) to_power k by A194, A99;
x in E by A194, XBOOLE_0:def 5;
then A203: ExtGp # x is non-decreasing by A35;
A204: (ExtGp # x) . n <= (ExtGp # x) . (n + 1) by A203;
ExtGp # x = Gp # x by MESFUN7C:1;
hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 by A195, A197, A204, A201, A202, A198, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 ; :: thesis: verum

end;

suppose A205: m1 <> 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

then consider m being Nat such that
A206: m1 = m + 1 by NAT_1:6;
reconsider m = m as Nat ;
0 < n1 by A194, A205;
then consider n being Nat such that
A207: n1 = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A208: m1 - 1 <= n1 - 1 by A194, XREAL_1:9;
x in E by A194, XBOOLE_0:def 5;
then A209: x in dom (G . n) by A17;
then A210: x in dom ((G . n) to_power k) by MESFUN6C:def 4;
(Gp # x) . n = (Gp . n) . x by SEQFUNC:def 10;
then (Gp # x) . n = ((G . n) to_power k) . x by A23;
then A211: (Gp # x) . n = ((G . n) . x) to_power k by A210, MESFUN6C:def 4;
G . n = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . n) by A16;
then (G . n) . x = ((abs (F1 . 0)) . x) + (((Partial_Sums AbsFMF) . n) . x) by A209, VALUED_1:def 1
.= |.((F1 . 0) . x).| + (((Partial_Sums AbsFMF) . n) . x) by VALUED_1:18 ;
then A212: (G . n) . x = |.((F1 . 0) . x).| + (((Partial_Sums AbsFMF) # x) . n) by SEQFUNC:def 10;
A213: ( (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n) & (F1 # x) . (m + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . m) ) by A194, A119;
A214: |.(((Partial_Sums (FMF # x)) . n) - ((Partial_Sums (FMF # x)) . m)).| <= (Partial_Sums (abs (FMF # x))) . n by Th10, A206, A207, A208;
A215: (Partial_Sums (abs (FMF # x))) . n = ((Partial_Sums AbsFMF) # x) . n by A111, A194;
0 <= |.((F1 . 0) . x).| by COMPLEX1:46;
then 0 + ((Partial_Sums (abs (FMF # x))) . n) <= |.((F1 . 0) . x).| + (((Partial_Sums AbsFMF) # x) . n) by A215, XREAL_1:6;
then A216: |.(((F1 # x) . (n + 1)) - ((F1 # x) . (m + 1))).| <= (G . n) . x by A212, A213, A214, XXREAL_0:2;
0 <= |.(((F1 # x) . (n + 1)) - ((F1 # x) . (m + 1))).| by COMPLEX1:46;
then A217: |.(((F1 # x) . (n + 1)) - ((F1 # x) . (m + 1))).| to_power k <= (Gp # x) . n by A211, A216, HOLDER_1:3;
x in E by A194, XBOOLE_0:def 5;
then A218: ExtGp # x is non-decreasing by A35;
A219: (ExtGp # x) . n <= (ExtGp # x) . (n + 1) by A218;
ExtGp # x = Gp # x by MESFUN7C:1;
hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 by A206, A207, A219, A217, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 ; :: thesis: verum

end;

A220: for x being Element of X
for n being Nat st x in E0 holds
|.((F . x) - ((F2 # x) . n)).| to_power k <= gp . x

proof

let x be Element of X; :: thesis: for n being Nat st x in E0 holds
|.((F . x) - ((F2 # x) . n)).| to_power k <= gp . x
let n1 be Nat; :: thesis: ( x in E0 implies |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x )
assume A221: x in E0 ; :: thesis: |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x
then A222: Gp # x is convergent by A94;
A223: F1 # x = F2 # x by A136, A221;
A224: F2 # x is convergent by A221, A134;
reconsider n = n1 as Nat ;
deffunc H₈( Nat) -> Element of REAL = ((F2 # x) . $1) - ((F2 # x) . n);
consider s0 being Real_Sequence such that
A225: for j being Nat holds s0 . j = H₈(j) from SEQ_1:sch 1();

A226: now :: thesis: for p being Real st 0 < p holds
ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))).| < p

let p be Real; :: thesis: ( 0 < p implies ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))).| < p )
assume 0 < p ; :: thesis: ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))).| < p
then consider n1 being Nat such that
A227: for m being Nat st n1 <= m holds
|.(((F2 # x) . m) - (lim (F2 # x))).| < p by A224, SEQ_2:def 7;
take n1 = n1; :: thesis: for m being Nat st n1 <= m holds
|.((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))).| < p
thus for m being Nat st n1 <= m holds
|.((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))).| < p :: thesis: verum

proof

let m be Nat; :: thesis: ( n1 <= m implies |.((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))).| < p )
assume A228: n1 <= m ; :: thesis: |.((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))).| < p
(s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n)) = (((F2 # x) . m) - ((F2 # x) . n)) - ((lim (F2 # x)) - ((F2 # x) . n)) by A225;
then (s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n)) = ((F2 # x) . m) - (lim (F2 # x)) ;
hence |.((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))).| < p by A228, A227; :: thesis: verum

end;

end;

then A229: s0 is convergent by SEQ_2:def 6;
then lim s0 = (lim (F2 # x)) - ((F2 # x) . n) by A226, SEQ_2:def 7;
then A230: lim (abs s0) = |.((lim (F2 # x)) - ((F2 # x) . n)).| by A229, SEQ_4:14;
A231: abs s0 is convergent by A229;
deffunc H₉( Nat) -> object = |.(((F2 # x) . $1) - ((F2 # x) . n)).| to_power k;
consider s being Real_Sequence such that
A232: for j being Nat holds s . j = H₉(j) from SEQ_1:sch 1();
A233: for j being Nat st n <= j holds
s . j <= (Gp # x) . j

proof

let j be Nat; :: thesis: ( n <= j implies s . j <= (Gp # x) . j )
assume n <= j ; :: thesis: s . j <= (Gp # x) . j
then |.(((F2 # x) . j) - ((F2 # x) . n)).| to_power k <= (Gp # x) . j by A223, A221, A193;
hence s . j <= (Gp # x) . j by A232; :: thesis: verum

end;

A234: now :: thesis: for n being Nat holds 0 <= (abs s0) . n

let n be Nat; :: thesis: 0 <= (abs s0) . n
0 <= |.(s0 . n).| by COMPLEX1:46;
hence 0 <= (abs s0) . n by VALUED_1:18; :: thesis: verum

end;

now :: thesis: for j being Nat holds s . j = ((abs s0) . j) to_power k

let j be Nat; :: thesis: s . j = ((abs s0) . j) to_power k
thus s . j = |.(((F2 # x) . j) - ((F2 # x) . n)).| to_power k by A232
.= |.(s0 . j).| to_power k by A225
.= ((abs s0) . j) to_power k by VALUED_1:18 ; :: thesis: verum

end;

then A235: ( s is convergent & lim s = (lim (abs s0)) to_power k ) by A234, A231, HOLDER_1:10;
then A236: ( s ^\ n is convergent & lim (s ^\ n) = lim s ) by SEQ_4:20;
gp . x = lim (Gp # x) by A152, A221;
then A237: ( (Gp # x) ^\ n is convergent & lim ((Gp # x) ^\ n) = gp . x ) by A222, SEQ_4:20;
for j being Nat holds (s ^\ n) . j <= ((Gp # x) ^\ n) . j

proof

let j be Nat; :: thesis: (s ^\ n) . j <= ((Gp # x) ^\ n) . j
( (s ^\ n) . j = s . (n + j) & ((Gp # x) ^\ n) . j = (Gp # x) . (n + j) ) by NAT_1:def 3;
hence (s ^\ n) . j <= ((Gp # x) ^\ n) . j by A233, NAT_1:11; :: thesis: verum

end;

then lim s <= gp . x by A236, A237, SEQ_2:18;
hence |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x by A230, A235, A147, A221; :: thesis: verum

end;

deffunc H₈( Nat) -> Element of bool [:X,REAL:] = |.(F - (F2 . $1)).| to_power k;
consider FP being Functional_Sequence of X,REAL such that
A238: for n being Nat holds FP . n = H₈(n) from SEQFUNC:sch 1();
A239: for n being Nat holds dom (FP . n) = E0

proof

let n1 be Nat; :: thesis: dom (FP . n1) = E0
reconsider n = n1 as Nat ;
A240: dom (F2 . n) = E0 by A138;
dom (FP . n1) = dom ((abs (F - (F2 . n))) to_power k) by A238;
then dom (FP . n1) = dom (abs (F - (F2 . n))) by MESFUN6C:def 4;
then dom (FP . n1) = dom (F - (F2 . n)) by VALUED_1:def 11;
then dom (FP . n1) = E0 /\ E0 by A240, A146, VALUED_1:12;
hence dom (FP . n1) = E0 ; :: thesis: verum

end;

then A241: E0 = dom (FP . 0) ;
then A242: dom (lim FP) = E0 by MESFUNC8:def 9;
for n, m being Nat holds dom (FP . n) = dom (FP . m)

proof

let n, m be Nat; :: thesis: dom (FP . n) = dom (FP . m)
thus dom (FP . n) = E0 by A239
.= dom (FP . m) by A239 ; :: thesis: verum

end;

then reconsider FP = FP as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
A243: for n being Nat holds FP . n is E0 -measurable

proof

let n1 be Nat; :: thesis: FP . n1 is E0 -measurable
reconsider n = n1 as Nat ;
dom (F2 . n) = E0 by A138;
then A244: dom (F - (F2 . n)) = E0 /\ E0 by A146, VALUED_1:12;
( F2 . n is E0 -measurable & dom (F2 . n) = E0 ) by A138;
then F - (F2 . n) is E0 -measurable by A190, MESFUNC6:29;
then A245: abs (F - (F2 . n)) is E0 -measurable by A244, MESFUNC6:48;
dom (abs (F - (F2 . n))) = E0 by A244, VALUED_1:def 11;
then (abs (F - (F2 . n))) to_power k is E0 -measurable by A245, MESFUN6C:29;
hence FP . n1 is E0 -measurable by A238; :: thesis: verum

end;

for x being Element of X
for n being Nat st x in E0 holds
|.(FP . n).| . x <= gp . x

proof

let x be Element of X; :: thesis: for n being Nat st x in E0 holds
|.(FP . n).| . x <= gp . x
let n1 be Nat; :: thesis: ( x in E0 implies |.(FP . n1).| . x <= gp . x )
reconsider n = n1 as Element of NAT by ORDINAL1:def 12;
assume A246: x in E0 ; :: thesis: |.(FP . n1).| . x <= gp . x
then A247: x in dom (FP . n) by A239;
then x in dom (|.(F - (F2 . n)).| to_power k) by A238;
then x in dom |.(F - (F2 . n)).| by MESFUN6C:def 4;
then A248: x in dom (F - (F2 . n)) by VALUED_1:def 11;
A249: FP . n1 = |.(F - (F2 . n1)).| to_power k by A238;
A250: 0 <= |.((F . x) - ((F2 . n1) . x)).| to_power k by Th4, COMPLEX1:46;
|.(FP . n).| . x = |.((FP . n) . x).| by VALUED_1:18
.= |.((|.(F - (F2 . n1)).| . x) to_power k).| by A247, A249, MESFUN6C:def 4
.= |.(|.((F - (F2 . n1)) . x).| to_power k).| by VALUED_1:18
.= |.(|.((F . x) - ((F2 . n1) . x)).| to_power k).| by A248, VALUED_1:13
.= |.((F . x) - ((F2 . n1) . x)).| to_power k by A250, ABSVALUE:def 1
.= |.((F . x) - ((F2 # x) . n)).| to_power k by SEQFUNC:def 10 ;
hence |.(FP . n1).| . x <= gp . x by A220, A246; :: thesis: verum

end;

then consider Ip being Real_Sequence such that
A251: ( ( for n being Nat holds Ip . n = Integral (M,(FP . n)) ) & ( ( for x being Element of X st x in E0 holds
FP # x is convergent ) implies ( Ip is convergent & lim Ip = Integral (M,(lim FP)) ) ) ) by A150, A155, A241, A243, MESFUN9C:48;
A252: for x being Element of X st x in E0 holds
( FP # x is convergent & lim (FP # x) = 0 )

proof

let x be Element of X; :: thesis: ( x in E0 implies ( FP # x is convergent & lim (FP # x) = 0 ) )
assume A253: x in E0 ; :: thesis: ( FP # x is convergent & lim (FP # x) = 0 )
A254: for n being Nat holds (FP # x) . n = |.((lim (F2 # x)) - ((F2 # x) . n)).| to_power k

proof

let n be Nat; :: thesis: (FP # x) . n = |.((lim (F2 # x)) - ((F2 # x) . n)).| to_power k
x in dom (FP . n) by A253, A239;
then A255: x in dom (|.(F - (F2 . n)).| to_power k) by A238;
then x in dom |.(F - (F2 . n)).| by MESFUN6C:def 4;
then A256: x in dom (F - (F2 . n)) by VALUED_1:def 11;
thus (FP # x) . n = (FP . n) . x by SEQFUNC:def 10
.= (|.(F - (F2 . n)).| to_power k) . x by A238
.= (|.(F - (F2 . n)).| . x) to_power k by A255, MESFUN6C:def 4
.= |.((F - (F2 . n)) . x).| to_power k by VALUED_1:18
.= |.((F . x) - ((F2 . n) . x)).| to_power k by A256, VALUED_1:13
.= |.((lim (F2 # x)) - ((F2 . n) . x)).| to_power k by A147, A253
.= |.((lim (F2 # x)) - ((F2 # x) . n)).| to_power k by SEQFUNC:def 10 ; :: thesis: verum

end;

F2 # x is convergent by A253, A134;
hence ( FP # x is convergent & lim (FP # x) = 0 ) by A254, Th11; :: thesis: verum

end;

A257: for x being Element of X st x in dom (lim FP) holds
0 = (lim FP) . x

proof

let x be Element of X; :: thesis: ( x in dom (lim FP) implies 0 = (lim FP) . x )
assume A258: x in dom (lim FP) ; :: thesis: 0 = (lim FP) . x
then A259: ( lim (FP # x) = 0 & FP # x is convergent ) by A252, A242;
(lim FP) . x = lim (R_EAL (FP # x)) by A258, MESFUN7C:14;
hence 0 = (lim FP) . x by A259, RINFSUP2:14; :: thesis: verum

end;

a.e-eq-class_Lp (F,M,k) in CosetSet (M,k) by A192;
then reconsider Sq0 = a.e-eq-class_Lp (F,M,k) as Point of (Lp-Space (M,k)) by Def11;
A260: for n being Nat holds Ip . n = ||.(Sq0 - (Sq . (N . n))).|| to_power k

proof

let n be Nat; :: thesis: Ip . n = ||.(Sq0 - (Sq . (N . n))).|| to_power k
set m = N . n;
reconsider n1 = n as Nat ;
A261: FP . n = (abs (F - (F2 . n1))) to_power k by A238;
A262: ( F in Lp_Functions (M,k) & F in Sq0 ) by A192, Th38;
( F2 . n1 in Lp_Functions (M,k) & F2 . n1 in Sq . (N . n) ) by A140;
then (- 1) (#) (F2 . n1) in (- 1) * (Sq . (N . n)) by Th54;
then F - (F2 . n1) in Sq0 + ((- 1) * (Sq . (N . n))) by Th54, A262;
then F - (F2 . n1) in Sq0 - (Sq . (N . n)) by RLVECT_1:16;
then consider r being Real such that
A263: ( 0 <= r & r = Integral (M,((abs (F - (F2 . n1))) to_power k)) & ||.(Sq0 - (Sq . (N . n))).|| = r to_power (1 / k) ) by Th53;
||.(Sq0 - (Sq . (N . n))).|| to_power k = r to_power ((1 / k) * k) by A263, HOLDER_1:2
.= r to_power 1 by XCMPLX_1:106
.= r by POWER:25 ;
hence Ip . n = ||.(Sq0 - (Sq . (N . n))).|| to_power k by A263, A261, A251; :: thesis: verum

end;

deffunc H₉( Nat) -> object = ||.(Sq0 - (Sq . (N . $1))).||;
consider Iq being Real_Sequence such that
A264: for n being Nat holds Iq . n = H₉(n) from SEQ_1:sch 1();
A265: for n being Nat holds Iq . n = ||.(Sq0 - (Sq . (N . n))).|| by A264;
( Iq is convergent & lim Iq = 0 )

proof

A266: for n being Nat holds Ip . n >= 0

proof

let n be Nat; :: thesis: Ip . n >= 0
||.(Sq0 - (Sq . (N . n))).|| to_power k >= 0 by Th4;
hence Ip . n >= 0 by A260; :: thesis: verum

end;

A267: for n being Nat holds Iq . n = (Ip . n) to_power (1 / k)

proof

let n be Nat; :: thesis: Iq . n = (Ip . n) to_power (1 / k)
thus (Ip . n) to_power (1 / k) = (||.(Sq0 - (Sq . (N . n))).|| to_power k) to_power (1 / k) by A260
.= ||.(Sq0 - (Sq . (N . n))).|| to_power (k * (1 / k)) by HOLDER_1:2
.= ||.(Sq0 - (Sq . (N . n))).|| to_power 1 by XCMPLX_1:106
.= ||.(Sq0 - (Sq . (N . n))).|| by POWER:25
.= Iq . n by A265 ; :: thesis: verum

end;

hence Iq is convergent by A266, A252, A251, HOLDER_1:10; :: thesis: lim Iq = 0
lim Iq = (lim Ip) to_power (1 / k) by A252, A251, A266, A267, HOLDER_1:10;
then lim Iq = 0 to_power (1 / k) by A252, A251, A257, A242, LPSPACE1:22;
hence lim Iq = 0 by POWER:def 2; :: thesis: verum

end;

hence Sq is convergent by A2, A265, Lm7; :: thesis: verum