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 V174() 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_{1}( 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_{1}(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) )

deffunc H_{2}( 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_{2}(n)
from SEQFUNC:sch 1();

A11: for n being Nat holds

( dom (FMF . n) = E & FMF . n in Lp_Functions (M,k) )

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 )

deffunc H_{3}( 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_{3}(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 )_{4}( 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_{4}(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 )

A26: for n being Nat holds

( dom (ExtGp . n) = E & ExtGp . n is E -measurable & ExtGp . n is nonnegative )

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

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

ExtGp # x is V176()

ExtGp # x is convergent

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;

then reconsider Ir = I as sequence of REAL by FUNCT_2:6;

deffunc H_{5}( Nat) -> Element of ExtREAL = Integral (M,((AbsFMF . $1) to_power k));

A42: for x being Element of NAT holds H_{5}(x) is Element of REAL

A43: for x being Element of NAT holds KPAbsFMF . x = H_{5}(x)
from FUNCT_2:sch 9(A42);

deffunc H_{6}( Nat) -> object = (KPAbsFMF . $1) to_power (1 / k);

A44: for x being Element of NAT holds H_{6}(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_{6}(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_{7}( Nat) -> set = (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . $1);

A46: for x being Element of NAT holds H_{7}(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_{7}(x)
from FUNCT_2:sch 9(A46);

A48: for n being Nat holds (Ir . n) to_power (1 / k) <= QAbsFMF . n

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 )

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

for n, m being Nat st n <= m holds

Ir . n <= Ir . m

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

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

( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) )

for n being Nat holds (Gp # x) . n = ((G # x) . n) to_power k

(Partial_Sums AbsFMF) # x is convergent

Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x

for n being Nat holds (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)

F1 # x is convergent

A134: for x being Element of X st x in E0 holds

(F1 || E0) # x is convergent

(F1 || E0) # x = F1 # x

( dom ((F1 || E0) . n) = E0 & (F1 || E0) . n is E0 -measurable )

A140: for n being Nat holds

( F2 . n in Lp_Functions (M,k) & F2 . n in Sq . (N . n) )

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)

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;

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)

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

for n being Nat st x in E0 holds

|.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| to_power k <= (Gp # x) . n

for n being Nat st x in E0 holds

|.((F2 # x) . n).| to_power k <= (Gp # x) . n

|.(((abs F) to_power k) . x).| <= gp . x

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

for n being Nat st x in E0 holds

|.((F . x) - ((F2 # x) . n)).| to_power k <= gp . x_{8}( 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_{8}(n)
from SEQFUNC:sch 1();

A239: for n being Nat holds dom (FP . n) = E0

then A242: dom (lim FP) = E0 by MESFUNC8:def 9;

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

A243: for n being Nat holds FP . n is E0 -measurable

for n being Nat st x in E0 holds

|.(FP . n).| . x <= gp . x

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 )

0 = (lim FP) . x

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_{9}( Nat) -> object = ||.(Sq0 - (Sq . (N . $1))).||;

consider Iq being Real_Sequence such that

A264: for n being Nat holds Iq . n = H_{9}(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 )

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

consider F1 being Functional_Sequence of X,REAL such that

A6: for n being Nat holds F1 . n = H

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

for n, m being Nat holds dom (F1 . n) = dom (F1 . m)
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;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

proof

then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
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;( dom (F1 . n) = E & dom (F1 . m) = E ) by A7;

hence dom (F1 . n) = dom (F1 . m) ; :: thesis: verum

deffunc H

consider FMF being Functional_Sequence of X,REAL such that

A10: for n being Nat holds FMF . n = H

A11: for n being Nat holds

( dom (FMF . n) = E & FMF . n in Lp_Functions (M,k) )

proof

for n, m being Nat holds dom (FMF . n) = dom (FMF . m)
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;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

proof

then reconsider FMF = FMF as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
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;( dom (FMF . n) = E & dom (FMF . m) = E ) by A11;

hence dom (FMF . n) = dom (FMF . m) ; :: thesis: verum

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

reconsider AbsFMF = abs FMF as with_the_same_dom Functional_Sequence of X,REAL by Th69;
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;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

deffunc H

consider G being Functional_Sequence of X,REAL such that

A16: for n being Nat holds G . n = H

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

deffunc H
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;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

consider Gp being Functional_Sequence of X,REAL such that

A23: for n being Nat holds Gp . n = H

A24: for n being Nat holds

( (G . n) to_power k is nonnegative & (G . n) to_power k is E -measurable )

proof

reconsider ExtGp = R_EAL Gp as Functional_Sequence of X,ExtREAL ;
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;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

A26: for n being Nat holds

( dom (ExtGp . n) = E & ExtGp . n is E -measurable & ExtGp . n is nonnegative )

proof

then A27:
( dom (ExtGp . 0) = E & ExtGp . 0 is nonnegative )
;
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;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

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

proof

then reconsider ExtGp = ExtGp as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
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;( dom (ExtGp . n) = E & dom (ExtGp . m) = E ) by A26;

hence dom (ExtGp . n) = dom (ExtGp . m) ; :: thesis: verum

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

A35:
for x being Element of X st x in E holds
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;(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

ExtGp # x is V176()

proof

A37:
for x being Element of X st x in E holds
let x be Element of X; :: thesis: ( x in E implies ExtGp # x is V176() )

assume A36: x in E ; :: thesis: ExtGp # x is V176()

for n, m being Nat st m <= n holds

(ExtGp # x) . m <= (ExtGp # x) . n

end;assume A36: x in E ; :: thesis: ExtGp # x is V176()

for n, m being Nat st m <= n holds

(ExtGp # x) . m <= (ExtGp # x) . n

proof

hence
ExtGp # x is V176()
by RINFSUP2:7; :: thesis: verum
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;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

ExtGp # x is convergent

proof

then consider I being ExtREAL_sequence such that
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 V176() by A35;

hence ExtGp # x is convergent by RINFSUP2:37; :: thesis: verum

end;assume x in E ; :: thesis: ExtGp # x is convergent

then ExtGp # x is V176() by A35;

hence ExtGp # x is convergent by RINFSUP2:37; :: thesis: verum

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

then
rng I c= REAL
;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;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

then reconsider Ir = I as sequence of REAL by FUNCT_2:6;

deffunc H

A42: for x being Element of NAT holds H

proof

consider KPAbsFMF being sequence of REAL such that
let x be Element of NAT ; :: thesis: H_{5}(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_{5}(x) is Element of REAL
by A13; :: thesis: verum

end;AbsFMF . x in Lp_Functions (M,k) by A13;

then Integral (M,((abs (AbsFMF . x)) to_power k)) in REAL by Th49;

hence H

A43: for x being Element of NAT holds KPAbsFMF . x = H

deffunc H

A44: for x being Element of NAT holds H

consider PAbsFMF being sequence of REAL such that

A45: for x being Element of NAT holds PAbsFMF . x = H

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

A46: for x being Element of NAT holds H

consider QAbsFMF being sequence of REAL such that

A47: for x being Element of NAT holds QAbsFMF . x = H

A48: for n being Nat holds (Ir . n) to_power (1 / k) <= QAbsFMF . n

proof

A63:
for n being Nat holds PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).||
defpred S_{1}[ 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_{1}[ 0 ]
by A1, A49, A51, A52, A53, Th61;

_{1}[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;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

A55: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

for n being Nat holds SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

A56: n in NAT by ORDINAL1:def 12;

assume S_{1}[n]
; :: thesis: S_{1}[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_{1}[n + 1]
by A62, A47; :: thesis: verum

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

assume S

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

hence for n being Nat holds (Ir . n) to_power (1 / k) <= QAbsFMF . n ; :: thesis: verum

proof

1 / 2 < 1
;
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;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

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

then
( PAbsFMF is summable & Sum PAbsFMF <= Sum ((1 / 2) GeoSeq) )
by A69, SERIES_1:20;
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;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

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

then A78:
Ir is bounded_above
by SEQ_2:def 3;
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;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

for n, m being Nat st n <= m holds

Ir . n <= Ir . m

proof

then
Ir is V176()
by SEQM_3:6;
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;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

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

A89:
eq_dom (LExtGp,+infty) = E /\ (eq_dom (LExtGp,+infty))
by A84, RELAT_1:132, XBOOLE_1:28;
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;

hence 0 <= LExtGp . x by A86, MESFUNC8:def 9; :: thesis: verum

end;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

then
0 <= lim (ExtGp # x1)
by A87, A37, MESFUNC9:10;let k1 be Nat; :: thesis: 0 <= (ExtGp # x1) . k1

reconsider k = k1 as Nat ;

ExtGp # x1 is V176() 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;reconsider k = k1 as Nat ;

ExtGp # x1 is V176() 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

hence 0 <= LExtGp . x by A86, MESFUNC8:def 9; :: thesis: verum

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

A94:
for x being Element of X st x in E0 holds
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;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

( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) )

proof

A99:
for x being Element of X st x in E0 holds
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;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

for n being Nat holds (Gp # x) . n = ((G # x) . n) to_power k

proof

A102:
for x being Element of X st x in E0 holds
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

end;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;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

(Partial_Sums AbsFMF) # x is convergent

proof

A111:
for x being Element of X st x in E0 holds
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;

then A106: G # x is convergent by A104, A105, Th9;

end;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

for n being Nat holds (Gp # x) . n = ((G # x) . n) to_power k
by A103, A99;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;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

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

hence
(Partial_Sums AbsFMF) # x is convergent
by SEQ_4:41; :: thesis: verumex 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;

for m being Nat st n <= m holds

|.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s ; :: thesis: verum

end;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

hence
ex n being Nat st |.((((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;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

for m being Nat st n <= m holds

|.((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)).| < s ; :: thesis: verum

Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x

proof

A119:
for x being Element of X st x in E0 holds
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_{1}[ 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_{1}[ 0 ]
;

_{1}[n]
from NAT_1:sch 2(A113, A114);

then for n being Element of NAT holds S_{1}[n]
;

hence Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x by FUNCT_2:63; :: thesis: verum

end;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

(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

A114: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

for n being Nat holds SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A115: S_{1}[n]
; :: thesis: S_{1}[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_{1}[n + 1]
; :: thesis: verum

end;assume A115: S

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

then for n being Element of NAT holds S

hence Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x by FUNCT_2:63; :: thesis: verum

for n being Nat holds (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)

proof

A128:
for x being Element of X st x in E0 holds
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_{1}[ 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_{1}[ 0 ]
by A122, SEQFUNC:def 10;

_{1}[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;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

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

A124: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

for n being Nat holds SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A125: S_{1}[n]
; :: thesis: S_{1}[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_{1}[n + 1]
by A127, SEQFUNC:def 10; :: thesis: verum

end;assume A125: S

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

hence for n being Nat holds (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n) ; :: thesis: verum

F1 # x is convergent

proof

set F2 = F1 || E0;
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;

end;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

hence
F1 # x is convergent
by SEQ_4:41; :: thesis: verumex 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;

for m being Nat st n <= m holds

|.(((F1 # x) . m) - ((F1 # x) . n)).| < s ; :: thesis: verum

end;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

hence
ex n being Nat st |.(((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;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

for m being Nat st n <= m holds

|.(((F1 # x) . m) - ((F1 # x) . n)).| < s ; :: thesis: verum

A134: for x being Element of X st x in E0 holds

(F1 || E0) # x is convergent

proof

A136:
for x being Element of X st x in E0 holds
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;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

(F1 || E0) # x = F1 # x

proof

A138:
for n being Nat holds
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

end;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

hence
(F1 || E0) # x = F1 # x
by FUNCT_2:63; :: thesis: verumlet 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;((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

( dom ((F1 || E0) . n) = E0 & (F1 || E0) . n is E0 -measurable )

proof

reconsider F2 = F1 || E0 as with_the_same_dom Functional_Sequence of X,REAL by MESFUN9C:2;
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

end;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

hence
(F1 || E0) . n is E0 -measurable
by A139, MESFUN9C:4, XBOOLE_1:36; :: thesis: verum
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;F1 . m is E -measurable by A7;

hence F1 . m is E0 -measurable by MESFUNC6:16, XBOOLE_1:36; :: thesis: verum

A140: for n being Nat holds

( F2 . n in Lp_Functions (M,k) & F2 . n in Sq . (N . n) )

proof

A145:
dom (lim F2) = dom (F2 . 0)
by MESFUNC8:def 9;
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;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

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

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

y in REAL

then
rng (lim F2) c= REAL
;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;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

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

then
rng (LExtGp | E0) c= REAL
;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;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

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

A154:
LExtGp is nonnegative
by A85, SUPINF_2:52;
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;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

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

A165:
for x being Element of X
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;|.((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

for n being Nat st x in E0 holds

|.(((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)).| to_power k <= (Gp # x) . n

proof

A170:
for x being Element of X
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;|.(((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

for n being Nat st x in E0 holds

|.((F2 # x) . n).| to_power k <= (Gp # x) . n

proof

A181:
for x being Element of X st x in E0 holds
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;

end;|.((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 )
;

end;

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

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 V176() 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;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 V176() 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

|.(((abs F) to_power k) . x).| <= gp . x

proof

R_EAL F is E0 -measurable
by A138, A156, A134, MESFUN7C:21;
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_{8}( 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_{8}(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 ;

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

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;assume A182: x in E0 ; :: thesis: |.(((abs F) to_power k) . x).| <= gp . x

then A183: Gp # x is convergent by A94;

deffunc H

consider s being Real_Sequence such that

A184: for n being Nat holds s . n = H

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

abs (F2 # x) is convergent
by A182, A134, SEQ_4:13;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;0 <= |.((F2 # x) . n).| by COMPLEX1:46;

hence 0 <= (abs (F2 # x)) . n by VALUED_1:18; :: thesis: verum

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

then A189:
((abs F) to_power k) . x <= gp . x
by A188, A185, A186, A183, SEQ_2:18;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;|.((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

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

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

A220:
for x being Element of X
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

end;|.(((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) . n1end;

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

end;

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

end;

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

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

end;

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

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 V176() 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;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 V176() 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

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 V176() 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;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 V176() 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

for n being Nat st x in E0 holds

|.((F . x) - ((F2 # x) . n)).| to_power k <= gp . x

proof

deffunc H
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_{8}( 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_{8}(j)
from SEQ_1:sch 1();

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_{9}( 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_{9}(j)
from SEQ_1:sch 1();

A233: for j being Nat st n <= j holds

s . j <= (Gp # x) . j

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

hence |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x by A230, A235, A147, A221; :: thesis: verum

end;|.((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

consider s0 being Real_Sequence such that

A225: for j being Nat holds s0 . j = H

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

then A229:
s0 is convergent
by SEQ_2:def 6;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

end;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;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

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

consider s being Real_Sequence such that

A232: for j being Nat holds s . j = H

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

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;0 <= |.(s0 . n).| by COMPLEX1:46;

hence 0 <= (abs s0) . n by VALUED_1:18; :: thesis: verum

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

then A235:
( s is convergent & lim s = (lim (abs s0)) to_power k )
by A234, A231, HOLDER_1:10;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;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

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

then
lim s <= gp . x
by A236, A237, SEQ_2:18;
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;( (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

hence |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x by A230, A235, A147, A221; :: thesis: verum

consider FP being Functional_Sequence of X,REAL such that

A238: for n being Nat holds FP . n = H

A239: for n being Nat holds dom (FP . n) = E0

proof

then A241:
E0 = dom (FP . 0)
;
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;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

then A242: dom (lim FP) = E0 by MESFUNC8:def 9;

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

proof

then reconsider FP = FP as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
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;thus dom (FP . n) = E0 by A239

.= dom (FP . m) by A239 ; :: thesis: verum

A243: for n being Nat holds FP . n is E0 -measurable

proof

for x being Element of X
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;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

for n being Nat st x in E0 holds

|.(FP . n).| . x <= gp . x

proof

then consider Ip being Real_Sequence such that
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;|.(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

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

A257:
for x being Element of X st x in dom (lim FP) holds
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

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

end;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

F2 # x is convergent
by A253, A134;
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;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

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

0 = (lim FP) . x

proof

a.e-eq-class_Lp (F,M,k) in CosetSet (M,k)
by A192;
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;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

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

deffunc H
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;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

consider Iq being Real_Sequence such that

A264: for n being Nat holds Iq . n = H

A265: for n being Nat holds Iq . n = ||.(Sq0 - (Sq . (N . n))).|| by A264;

( Iq is convergent & lim Iq = 0 )

proof

hence
Sq is convergent
by A2, A265, Lm7; :: thesis: verum
A266:
for n being Nat holds Ip . n >= 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;proof

A267:
for n being Nat holds Iq . n = (Ip . n) to_power (1 / k)
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;||.(Sq0 - (Sq . (N . n))).|| to_power k >= 0 by Th4;

hence Ip . n >= 0 by A260; :: thesis: verum

proof

hence
Iq is convergent
by A266, A252, A251, HOLDER_1:10; :: thesis: lim Iq = 0
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;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

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