defpred S₁[ non zero Nat] means for D being $1 -element FinSequence
for f being PartFunc of (CarProduct ((Seg $1) --> RNS_Real)),RNS_Real
for g being PartFunc of (CarProduct ((Seg $1) --> REAL)),REAL st f = g & ( for i being Nat st i in Seg $1 holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D holds
g is_integrable_on Prod_Measure (L-Meas $1);
A1: S₁[1]

proof

let D be 1 -element FinSequence; :: thesis: for f being PartFunc of (CarProduct ((Seg 1) --> RNS_Real)),RNS_Real
for g being PartFunc of (CarProduct ((Seg 1) --> REAL)),REAL st f = g & ( for i being Nat st i in Seg 1 holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D holds
g is_integrable_on Prod_Measure (L-Meas 1)
let f be PartFunc of (CarProduct ((Seg 1) --> RNS_Real)),RNS_Real; :: thesis: for g being PartFunc of (CarProduct ((Seg 1) --> REAL)),REAL st f = g & ( for i being Nat st i in Seg 1 holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D holds
g is_integrable_on Prod_Measure (L-Meas 1)
let g be PartFunc of (CarProduct ((Seg 1) --> REAL)),REAL; :: thesis: ( f = g & ( for i being Nat st i in Seg 1 holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D implies g is_integrable_on Prod_Measure (L-Meas 1) )
assume that
A2: f = g and
A3: for i being Nat st i in Seg 1 holds
D . i is closed_interval Subset of REAL and
A4: f is_continuous_on CarProduct D and
A5: dom f = CarProduct D ; :: thesis: g is_integrable_on Prod_Measure (L-Meas 1)
1 in Seg 1 ;
then reconsider I = D . 1 as closed_interval Subset of REAL by A3;
reconsider f0 = f as PartFunc of RNS_Real,RNS_Real by Th13;
reconsider g0 = g as PartFunc of REAL,REAL by MEASUR14:37;
A6: CarProduct D = I by MEASUR13:def 3;
A7: I is Element of L-Field by MEASUR12:72, MEASUR12:75;

now :: thesis: for x0, r being Real st x0 in I & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - x0).| < s holds
|.((g0 . x1) - (g0 . x0)).| < r ) )

let x0, r be Real; :: thesis: ( x0 in I & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - x0).| < s holds
|.((g0 . x1) - (g0 . x0)).| < r ) ) )
assume A8: ( x0 in I & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - x0).| < s holds
|.((g0 . x1) - (g0 . x0)).| < r ) )
reconsider p = x0 as Point of RNS_Real by XREAL_0:def 1;
reconsider pt = p as Point of (CarProduct ((Seg 1) --> RNS_Real)) by Th13;
f | I is_continuous_in pt by A4, A6, A8;
then consider s being Real such that
A9: ( 0 < s & ( for p1 being Point of RNS_Real st p1 in dom (f0 | I) & ||.(p1 - p).|| < s holds
||.(((f0 | I) /. p1) - ((f0 | I) /. p)).|| < r ) ) by A8, Th13, NFCONT_1:7;
take s = s; :: thesis: ( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - x0).| < s holds
|.((g0 . x1) - (g0 . x0)).| < r ) )
thus 0 < s by A9; :: thesis: for x1 being Real st x1 in I & |.(x1 - x0).| < s holds
|.((g0 . x1) - (g0 . x0)).| < r

hereby :: thesis: verum

let x1 be Real; :: thesis: ( x1 in I & |.(x1 - x0).| < s implies |.((g0 . x1) - (g0 . x0)).| < r )
assume A10: ( x1 in I & |.(x1 - x0).| < s ) ; :: thesis: |.((g0 . x1) - (g0 . x0)).| < r
reconsider p1 = x1 as Point of RNS_Real by XREAL_0:def 1;
p1 - p = x1 - x0 by DUALSP03:4;
then ||.(p1 - p).|| = |.(x1 - x0).| by EUCLID:def 2;
then A11: ||.(((f0 | I) /. p1) - ((f0 | I) /. p)).|| < r by A5, A6, A9, A10;
A12: (f0 | I) /. p1 = g0 . x1 by A2, A5, A6, A10, PARTFUN1:def 6;
(f0 | I) /. p = g0 . x0 by A2, A5, A6, A8, PARTFUN1:def 6;
then ((f0 | I) /. p1) - ((f0 | I) /. p) = (g0 . x1) - (g0 . x0) by A12, DUALSP03:4;
hence |.((g0 . x1) - (g0 . x0)).| < r by A11, EUCLID:def 2; :: thesis: verum

end;

end;

then A13: g0 | I is continuous by A2, A5, A6, FCONT_1:14;

per cases ( I <> {} or I = {} ) ;

suppose I <> {} ; :: thesis: g is_integrable_on Prod_Measure (L-Meas 1)

then reconsider I = I as non empty closed_interval Subset of REAL ;
( g0 || I is bounded & g0 is_integrable_on I ) by A2, A5, A6, A13, INTEGRA5:10, INTEGRA5:11;
hence g is_integrable_on Prod_Measure (L-Meas 1) by A2, A5, A6, A7, MESFUN14:49, MEASUR14:37, MEASUR14:41, MEASUR14:45; :: thesis: verum

end;

suppose I = {} ; :: thesis: g is_integrable_on Prod_Measure (L-Meas 1)

hence g is_integrable_on Prod_Measure (L-Meas 1) by A2, A5, Th1, MEASUR13:def 3; :: thesis: verum

end;

end;

end;

A14: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A15: S₁[n] ; :: thesis: S₁[n + 1]
let D be n + 1 -element FinSequence; :: thesis: for f being PartFunc of (CarProduct ((Seg (n + 1)) --> RNS_Real)),RNS_Real
for g being PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL st f = g & ( for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D holds
g is_integrable_on Prod_Measure (L-Meas (n + 1))
let f be PartFunc of (CarProduct ((Seg (n + 1)) --> RNS_Real)),RNS_Real; :: thesis: for g being PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL st f = g & ( for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D holds
g is_integrable_on Prod_Measure (L-Meas (n + 1))
let g be PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL; :: thesis: ( f = g & ( for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D implies g is_integrable_on Prod_Measure (L-Meas (n + 1)) )
assume that
A16: f = g and
A17: for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL and
A18: f is_continuous_on CarProduct D and
A19: dom f = CarProduct D ; :: thesis: g is_integrable_on Prod_Measure (L-Meas (n + 1))
reconsider f0 = f as PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real by MEASUR15:38;
A20: f0 is_continuous_on dom f0 by A18, A19, MEASUR15:38;
A21: CarProduct ((Seg (n + 1)) --> REAL) = [:(CarProduct ((Seg n) --> REAL)),REAL:] by MEASUR15:38;
reconsider g0 = g as PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL by MEASUR15:38;
set Rg0 = R_EAL g0;
for i being Nat st i in Seg (n + 1) holds
D . i is Interval by A17;
then reconsider E = CarProduct D as Element of Prod_Field (L-Field (n + 1)) by Th9;
A22: ( g is E -measurable & dom g = E & ( for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x, y being n + 1 -element FinSequence of REAL st PtCarProduct x in CarProduct D & PtCarProduct y in CarProduct D & ( for i being Nat st i in dom D holds
ex xi, yi being Real st
( xi = x . i & yi = y . i & |.(xi - yi).| < r ) ) holds
|.((g . (PtCarProduct x)) - (g . (PtCarProduct y))).| < e ) ) ) ) by A16, A17, A18, A19, Th42, MEASUR15:66;
A23: D . (n + 1) is closed_interval Subset of REAL by A17, FINSEQ_1:4;
then consider s, t being Real such that
A24: D . (n + 1) = [.s,t.] by MEASURE5:def 3;

per cases ( s <= t or s > t ) ;

suppose s <= t ; :: thesis: g is_integrable_on Prod_Measure (L-Meas (n + 1))

then A25: [.s,t.] = ['s,t'] by INTEGRA5:def 3;
reconsider J = ['s,t'] as Element of L-Field by MEASUR10:5, MEASUR12:75;
reconsider D1 = D | n as n -element FinSequence ;
A26: CarProduct D = [:(CarProduct D1),[.s,t.]:] by A24, Th4;
A27: for i being Nat st i in Seg n holds
D1 . i c= ((Seg n) --> REAL) . i

proof

let i be Nat; :: thesis: ( i in Seg n implies D1 . i c= ((Seg n) --> REAL) . i )
assume A28: i in Seg n ; :: thesis: D1 . i c= ((Seg n) --> REAL) . i
then A29: i <= n by FINSEQ_1:1;
Seg n c= Seg (n + 1) by NAT_1:11, FINSEQ_1:5;
then D . i is closed_interval Subset of REAL by A17, A28;
then D . i c= REAL ;
then D1 . i c= REAL by A29, FINSEQ_3:112;
hence D1 . i c= ((Seg n) --> REAL) . i by A28, FUNCOP_1:7; :: thesis: verum

end;

then A30: CarProduct D1 is Subset of (CarProduct ((Seg n) --> REAL)) by Th10;
A31: dom (R_EAL g0) = [:(CarProduct D1),[.s,t.]:] by A26, A16, A19, MESFUNC5:def 7;
then A32: dom |.(R_EAL g0).| = [:(CarProduct D1),[.s,t.]:] by MESFUNC1:def 10;
A33: for x being Element of CarProduct ((Seg n) --> REAL) st x in (CarProduct ((Seg n) --> REAL)) \ (CarProduct D1) holds
( dom (ProjPMap1 (|.(R_EAL g0).|,x)) = {} & (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = 0 )

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis: ( x in (CarProduct ((Seg n) --> REAL)) \ (CarProduct D1) implies ( dom (ProjPMap1 (|.(R_EAL g0).|,x)) = {} & (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = 0 ) )
assume x in (CarProduct ((Seg n) --> REAL)) \ (CarProduct D1) ; :: thesis: ( dom (ProjPMap1 (|.(R_EAL g0).|,x)) = {} & (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = 0 )
then not x in CarProduct D1 by XBOOLE_0:def 5;
hence dom (ProjPMap1 (|.(R_EAL g0).|,x)) = {} by A30, A32, MESFUN16:25; :: thesis: (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = 0
then Integral (L-Meas,(ProjPMap1 (|.(R_EAL g0).|,x))) = 0 by MESFUN16:1;
hence (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = 0 by MESFUN12:def 8; :: thesis: verum

end;

A34: for x being Element of CarProduct ((Seg n) --> REAL)
for y being Element of REAL st x in CarProduct D1 & y in [.s,t.] holds
( (ProjPMap1 (|.(R_EAL g0).|,x)) . y = |.(R_EAL g0).| . (x,y) & |.(R_EAL g0).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g0).| . (x,y) = |.g.| . [x,y] )

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis: for y being Element of REAL st x in CarProduct D1 & y in [.s,t.] holds
( (ProjPMap1 (|.(R_EAL g0).|,x)) . y = |.(R_EAL g0).| . (x,y) & |.(R_EAL g0).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g0).| . (x,y) = |.g.| . [x,y] )
let y be Element of REAL ; :: thesis: ( x in CarProduct D1 & y in [.s,t.] implies ( (ProjPMap1 (|.(R_EAL g0).|,x)) . y = |.(R_EAL g0).| . (x,y) & |.(R_EAL g0).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g0).| . (x,y) = |.g.| . [x,y] ) )
assume A35: ( x in CarProduct D1 & y in [.s,t.] ) ; :: thesis: ( (ProjPMap1 (|.(R_EAL g0).|,x)) . y = |.(R_EAL g0).| . (x,y) & |.(R_EAL g0).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g0).| . (x,y) = |.g.| . [x,y] )
hence (ProjPMap1 (|.(R_EAL g0).|,x)) . y = |.(R_EAL g0).| . (x,y) by A32, ZFMISC_1:87, MESFUN12:def 3; :: thesis: ( |.(R_EAL g0).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g0).| . (x,y) = |.g.| . [x,y] )
[x,y] in dom g by A35, A26, A16, A19, ZFMISC_1:87;
then A36: [x,y] in dom |.g.| by VALUED_1:def 11;
A37: (R_EAL g0) . [x,y] = g . [x,y] by MESFUNC5:def 7;
|.(R_EAL g0).| . (x,y) = |.((R_EAL g0) . [x,y]).| by A35, A32, ZFMISC_1:87, MESFUNC1:def 10;
hence |.(R_EAL g0).| . (x,y) = |.(g . [x,y]).| by A37, EXTREAL1:12; :: thesis: |.(R_EAL g0).| . (x,y) = |.g.| . [x,y]
hence |.(R_EAL g0).| . (x,y) = |.g.| . [x,y] by VALUED_1:def 11, A36; :: thesis: verum

end;

A38: for x being Element of CarProduct ((Seg n) --> REAL) st x in CarProduct D1 holds
0 <= (Integral2 (L-Meas,|.(R_EAL g0).|)) . x

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis: ( x in CarProduct D1 implies 0 <= (Integral2 (L-Meas,|.(R_EAL g0).|)) . x )
assume A39: x in CarProduct D1 ; :: thesis: 0 <= (Integral2 (L-Meas,|.(R_EAL g0).|)) . x
reconsider Pg = ProjPMap1 (|.(R_EAL g0).|,x) as PartFunc of REAL,REAL by MESFUN16:30;
A40: dom Pg = ['s,t'] by A25, A39, A30, A32, MESFUN16:25;
then A41: ( Pg || ['s,t'] is bounded & Pg is_integrable_on ['s,t'] ) by A16, A20, Th25, INTEGRA5:10, INTEGRA5:11;
A42: integral (Pg,s,t) = Integral (L-Meas,(Pg | [.s,t.])) by A40, A25, A41, XXREAL_1:29, MESFUN14:50;
then integral (Pg,s,t) = Integral (L-Meas,(ProjPMap1 (|.(R_EAL g0).|,x))) by A40, A25, MESFUNC5:def 7;
then A43: (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = integral (Pg,s,t) by MESFUN12:def 8;
A44: Pg = R_EAL (Pg | [.s,t.]) by A25, A40, MESFUNC5:def 7;
[.s,t.] is Element of L-Field by MEASUR10:5, MEASUR12:75;
then Pg | [.s,t.] is_integrable_on L-Meas by A40, A25, A41, MESFUN14:49;
then ex A being Element of L-Field st
( A = dom (R_EAL (Pg | [.s,t.])) & R_EAL (Pg | [.s,t.]) is A -measurable ) by MESFUNC5:def 17;
then A45: ( J = dom (Pg | [.s,t.]) & Pg | [.s,t.] is J -measurable ) by A40, A44, MESFUNC5:def 7;
for y being object st y in dom (Pg | [.s,t.]) holds
0 <= (Pg | [.s,t.]) . y

proof

let y be object ; :: thesis: ( y in dom (Pg | [.s,t.]) implies 0 <= (Pg | [.s,t.]) . y )
assume A46: y in dom (Pg | [.s,t.]) ; :: thesis: 0 <= (Pg | [.s,t.]) . y
then reconsider y1 = y as Element of REAL ;
( (ProjPMap1 (|.(R_EAL g0).|,x)) . y = |.(R_EAL g0).| . (x,y1) & |.(R_EAL g0).| . (x,y1) = |.(g . [x,y1]).| ) by A39, A25, A40, A46, A34;
hence 0 <= (Pg | [.s,t.]) . y by A25, A40; :: thesis: verum

end;

hence 0 <= (Integral2 (L-Meas,|.(R_EAL g0).|)) . x by A42, A43, A45, MESFUNC6:52, MESFUNC6:84; :: thesis: verum

end;

set G2 = Integral2 (L-Meas,|.(R_EAL g0).|);
A47: dom (Integral2 (L-Meas,|.(R_EAL g0).|)) = CarProduct ((Seg n) --> REAL) by FUNCT_2:def 1;
then A48: dom ((Integral2 (L-Meas,|.(R_EAL g0).|)) | (CarProduct D1)) = CarProduct D1 by A27, Th10, RELAT_1:62;
reconsider G2I = (Integral2 (L-Meas,|.(R_EAL g0).|)) | (CarProduct D1) as PartFunc of (CarProduct ((Seg n) --> REAL)),ExtREAL ;

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

let y be object ; :: thesis: ( y in rng G2I implies y in REAL )
assume y in rng G2I ; :: thesis: y in REAL
then consider x being object such that
A49: ( x in dom G2I & y = G2I . x ) by FUNCT_1:def 3;
reconsider x = x as Element of CarProduct ((Seg n) --> REAL) by A49;
reconsider Pg = ProjPMap1 (|.(R_EAL g0).|,x) as PartFunc of REAL,REAL by MESFUN16:30;
A50: dom Pg = ['s,t'] by A25, A49, A48, A32, MESFUN16:25;
then A51: Pg || ['s,t'] is bounded by A16, A20, Th25, INTEGRA5:10;
Pg is_integrable_on ['s,t'] by A16, A20, A50, Th25, INTEGRA5:11;
then integral (Pg,s,t) = Integral (L-Meas,(Pg | [.s,t.])) by A50, A25, A51, XXREAL_1:29, MESFUN14:50;
then integral (Pg,s,t) = Integral (L-Meas,(ProjPMap1 (|.(R_EAL g0).|,x))) by A50, A25, MESFUNC5:def 7;
then (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = integral (Pg,s,t) by MESFUN12:def 8;
then (Integral2 (L-Meas,|.(R_EAL g0).|)) . x in REAL by XREAL_0:def 1;
hence y in REAL by A49, A48, FUNCT_1:49; :: thesis: verum

end;

then ( rng G2I c= REAL & dom G2I c= CarProduct ((Seg n) --> REAL) ) ;
then reconsider G = G2I as PartFunc of (CarProduct ((Seg n) --> REAL)),REAL by RELSET_1:4;
A52: dom G = CarProduct D1 by A47, A27, Th10, RELAT_1:62;
reconsider GG = G as PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real by MEASUR15:42;
A53: for i being Nat st i in Seg n holds
D1 . i is closed_interval Subset of REAL

proof

let i be Nat; :: thesis: ( i in Seg n implies D1 . i is closed_interval Subset of REAL )
assume A54: i in Seg n ; :: thesis: D1 . i is closed_interval Subset of REAL
then i <= n by FINSEQ_1:1;
then A55: D1 . i = D . i by FINSEQ_3:112;
Seg n c= Seg (n + 1) by FINSEQ_3:18;
hence D1 . i is closed_interval Subset of REAL by A54, A55, A17; :: thesis: verum

end;

CarProduct D1 is Subset of (CarProduct ((Seg n) --> RNS_Real)) by A30, MEASUR15:42;
then GG is_continuous_on CarProduct D1 by A16, A19, A20, A26, A23, A24, A53, Th40;
then G is_integrable_on Prod_Measure (L-Meas n) by A15, A53, RELAT_1:62;
then A56: G2I is_integrable_on Prod_Measure (L-Meas n) by MESFUNC5:def 7;
then A57: Integral ((Prod_Measure (L-Meas n)),G2I) < +infty by MESFUNC5:96;
A58: for i being Nat st i in Seg n holds
D1 . i is Interval by A53;
then reconsider AB = CarProduct D1 as Element of Prod_Field (L-Field n) by Th9;
CarProduct ((Seg n) --> REAL) in Prod_Field (L-Field n) by PROB_1:5;
then reconsider NAB = (CarProduct ((Seg n) --> REAL)) \ AB as Element of Prod_Field (L-Field n) by PROB_1:6;
A59: AB \/ NAB = CarProduct ((Seg n) --> REAL) by XBOOLE_1:45;
A60: AB /\ NAB = {} by XBOOLE_1:85, XBOOLE_0:def 7;
A61: for r being Element of CarProduct ((Seg n) --> REAL) holds 0. <= (Integral2 (L-Meas,|.(R_EAL g0).|)) . r

proof

let r be Element of CarProduct ((Seg n) --> REAL); :: thesis: 0. <= (Integral2 (L-Meas,|.(R_EAL g0).|)) . r
( r in AB or r in NAB ) by A59, XBOOLE_0:def 3;
hence 0 <= (Integral2 (L-Meas,|.(R_EAL g0).|)) . r by A33, A38; :: thesis: verum

end;

then A62: Integral2 (L-Meas,|.(R_EAL g0).|) is nonnegative ;
reconsider H = CarProduct ((Seg n) --> REAL) as Element of Prod_Field (L-Field n) by PROB_1:5;
A63: dom (Integral2 (L-Meas,|.(R_EAL g0).|)) = H by FUNCT_2:def 1;
for r being Real holds H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)) in Prod_Field (L-Field n)

proof

let r be Real; :: thesis: H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)) in Prod_Field (L-Field n)
A64: ex H0 being Element of Prod_Field (L-Field n) st
( H0 = dom G2I & G2I is H0 -measurable ) by A56, MESFUNC5:def 17;

per cases ( r <= 0 or 0 < r ) ;

suppose A65: r <= 0 ; :: thesis: H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)) in Prod_Field (L-Field n)

now :: thesis: not less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r) <> {}

assume less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r) <> {} ; :: thesis: contradiction
then consider x being object such that
A66: x in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r) by XBOOLE_0:def 1;
( x in dom (Integral2 (L-Meas,|.(R_EAL g0).|)) & (Integral2 (L-Meas,|.(R_EAL g0).|)) . x < r ) by A66, MESFUNC1:def 11;
hence contradiction by A61, A65; :: thesis: verum

end;

hence H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)) in Prod_Field (L-Field n) by PROB_1:4; :: thesis: verum

end;

suppose A67: 0 < r ; :: thesis: H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)) in Prod_Field (L-Field n)

A68: for z being object holds
( z in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r) iff z in (less_dom (G2I,r)) \/ NAB )

proof

let z be object ; :: thesis: ( z in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r) iff z in (less_dom (G2I,r)) \/ NAB )

hereby :: thesis: ( z in (less_dom (G2I,r)) \/ NAB implies z in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r) )

assume A69: z in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r) ; :: thesis: z in (less_dom (G2I,r)) \/ NAB
then A70: ( z in dom (Integral2 (L-Meas,|.(R_EAL g0).|)) & (Integral2 (L-Meas,|.(R_EAL g0).|)) . z < r ) by MESFUNC1:def 11;
A71: ( z in AB or z in NAB ) by A59, A69, XBOOLE_0:def 3;

now :: thesis: ( z in AB implies z in (less_dom (G2I,r)) \/ NAB )

assume A72: z in AB ; :: thesis: z in (less_dom (G2I,r)) \/ NAB
then G2I . z < r by FUNCT_1:49, A70;
then z in less_dom (G2I,r) by A72, A52, MESFUNC1:def 11;
hence z in (less_dom (G2I,r)) \/ NAB by XBOOLE_0:def 3; :: thesis: verum

end;

hence z in (less_dom (G2I,r)) \/ NAB by A71, XBOOLE_0:def 3; :: thesis: verum

end;

assume z in (less_dom (G2I,r)) \/ NAB ; :: thesis: z in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)

per cases then ( z in less_dom (G2I,r) or z in NAB ) by XBOOLE_0:def 3;

suppose A73: z in less_dom (G2I,r) ; :: thesis: z in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)

then ( z in dom G2I & G2I . z < r ) by MESFUNC1:def 11;
then (Integral2 (L-Meas,|.(R_EAL g0).|)) . z < r by A52, FUNCT_1:49;
hence z in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r) by A63, A73, MESFUNC1:def 11; :: thesis: verum

end;

suppose A74: z in NAB ; :: thesis: z in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)

then reconsider x = z as Element of CarProduct ((Seg n) --> REAL) ;
(Integral2 (L-Meas,|.(R_EAL g0).|)) . x = 0 by A74, A33;
hence z in less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r) by A63, A67, MESFUNC1:def 11; :: thesis: verum

end;

end;

end;

A75: H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)) = (AB \/ NAB) /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)) by XBOOLE_1:45
.= (AB \/ NAB) /\ ((less_dom (G2I,r)) \/ NAB) by A68, TARSKI:2
.= (AB /\ ((less_dom (G2I,r)) \/ NAB)) \/ (NAB /\ ((less_dom (G2I,r)) \/ NAB)) by XBOOLE_1:23 ;
AB /\ ((less_dom (G2I,r)) \/ NAB) = (AB /\ (less_dom (G2I,r))) \/ {} by A60, XBOOLE_1:23;
then A76: AB /\ ((less_dom (G2I,r)) \/ NAB) in Prod_Field (L-Field n) by A64, A47;
A77: less_dom (G2I,r) c= AB by MESFUNC1:def 11, A52;
NAB /\ ((less_dom (G2I,r)) \/ NAB) = (NAB /\ (less_dom (G2I,r))) \/ (NAB /\ NAB) by XBOOLE_1:23;
then NAB /\ ((less_dom (G2I,r)) \/ NAB) = {} \/ (NAB /\ NAB) by A77;
hence H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g0).|)),r)) in Prod_Field (L-Field n) by A75, A76, PROB_1:3; :: thesis: verum

end;

end;

end;

then A78: Integral2 (L-Meas,|.(R_EAL g0).|) is H -measurable ;
reconsider G2J = (Integral2 (L-Meas,|.(R_EAL g0).|)) | NAB as PartFunc of (CarProduct ((Seg n) --> REAL)),ExtREAL by PARTFUN1:11;
(Integral2 (L-Meas,|.(R_EAL g0).|)) | (AB \/ NAB) = Integral2 (L-Meas,|.(R_EAL g0).|) by A59;
then A79: Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,|.(R_EAL g0).|))) = (Integral ((Prod_Measure (L-Meas n)),G2I)) + (Integral ((Prod_Measure (L-Meas n)),G2J)) by A63, A78, A62, XBOOLE_1:79, MESFUNC5:91;
for x being object st x in dom G2J holds
G2J . x = 0

proof

let x be object ; :: thesis: ( x in dom G2J implies G2J . x = 0 )
assume A80: x in dom G2J ; :: thesis: G2J . x = 0
then reconsider r = x as Element of CarProduct ((Seg n) --> REAL) ;
(Integral2 (L-Meas,|.(R_EAL g0).|)) . r = 0 by A80, A33, A47;
hence G2J . x = 0 by FUNCT_1:49, A80, A47; :: thesis: verum

end;

then Integral ((Prod_Measure (L-Meas n)),G2J) = 0 * ((Prod_Measure (L-Meas n)) . (dom G2J)) by A47, MEASUR10:27;
then A81: Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,|.(R_EAL g0).|))) < +infty by A57, A79, XXREAL_3:4;
CarProduct D1 is Element of Prod_Field (L-Field n) by A58, Th9;
then ( CarProduct D1 in Prod_Field (L-Field n) & [.s,t.] in L-Field ) by MEASUR10:5, MEASUR12:75;
then A82: [:(CarProduct D1),[.s,t.]:] in measurable_rectangles ((Prod_Field (L-Field n)),L-Field) ;
measurable_rectangles ((Prod_Field (L-Field n)),L-Field) c= sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by PROB_1:def 9;
then reconsider E0 = [:(CarProduct D1),[.s,t.]:] as Element of sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by A82;
A83: Prod_Field (L-Field (n + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by MEASUR14:44;
then reconsider Rg0 = R_EAL g0 as E0 -measurable PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],ExtREAL by A22, A21, A26;
Prod_Measure (L-Meas n) is sigma_finite by MEASUR15:36;
then Rg0 is_integrable_on Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) by A31, MESFUN16:5, A81, MESFUN13:11;
hence g is_integrable_on Prod_Measure (L-Meas (n + 1)) by A21, A83, MEASUR14:48; :: thesis: verum

end;

suppose s > t ; :: thesis: g is_integrable_on Prod_Measure (L-Meas (n + 1))

then A84: D . (n + 1) = {} by A24, XXREAL_1:29;
n < n + 1 by NAT_1:13;
then (ProdFinSeq D) . (n + 1) = [:((ProdFinSeq D) . n),(D . (n + 1)):] by MEASUR13:def 3;
then CarProduct D = {} by A84;
hence g is_integrable_on Prod_Measure (L-Meas (n + 1)) by A16, A19, Th1; :: thesis: verum

end;

end;

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A1, A14);
hence for n being non zero Nat
for D being b₁ -element FinSequence
for f being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for g being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st f = g & ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D holds
g is_integrable_on Prod_Measure (L-Meas n) ; :: thesis: verum