let n be non zero Nat; :: thesis:
defpred S₁[ non zero Nat] means for D being $1 -element FinSequence st ( for i being Nat st i in Seg $1 holds
D . i is closed_interval Subset of REAL ) holds
ex r being Real ex E being Element of Prod_Field (L-Field $1) st
( E = CarProduct D & (Prod_Measure (L-Meas $1)) . E = r & 0 <= r );
A1: S₁[1]

proof

let D be 1 -element FinSequence; :: thesis:
assume A2: for i being Nat st i in Seg 1 holds
D . i is closed_interval Subset of REAL ; :: thesis:
A3: 1 in Seg 1 ;
A4: CarProduct D = D . 1 by MEASUR13:def 3;
then A5: CarProduct D is closed_interval Subset of REAL by A2, A3;
then reconsider E = CarProduct D as Element of Prod_Field (L-Field 1) by MEASUR14:41;

per cases ;

suppose A6: D . 1 <> {} ; :: thesis:

consider a, b being Real such that
A7: E = [.a,b.] by A5, MEASURE5:def 3;
A8: a <= b by A7, A4, A6, XXREAL_1:29;
set r = b - a;
take b - a ; :: thesis:
take E ; :: thesis:
thus E = CarProduct D ; :: thesis:
thus (Prod_Measure (L-Meas 1)) . E = b - a by A7, A8, MESFUN14:5, MEASUR14:45; :: thesis:
thus 0 <= b - a by A7, A4, A6, XXREAL_1:29, XREAL_1:48; :: thesis:

end;

suppose A9: D . 1 = {} ; :: thesis:

reconsider E = {} as Element of Prod_Field (L-Field 1) by MEASURE1:7;
set r = 0 ;
take 0 ; :: thesis:
take E ; :: thesis:
thus E = CarProduct D by A9, MEASUR13:def 3; :: thesis:
thus (Prod_Measure (L-Meas 1)) . E = 0 by VALUED_0:def 19; :: thesis:
thus 0 <= 0 ; :: thesis:

end;

end;

end;

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

proof

let n be non zero Nat; :: thesis:
assume A11: S₁[n] ; :: thesis:
let D be n + 1 -element FinSequence; :: thesis:
assume A12: for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL ; :: thesis:
reconsider D1 = D | n as n -element FinSequence ;
for i being Nat st i in Seg n holds
D1 . i is closed_interval Subset of REAL

proof

let i be Nat; :: thesis:
assume A13: i in Seg n ; :: thesis:
A14: Seg n c= Seg (n + 1) by FINSEQ_3:18;
D1 . i = D . i by A13, FUNCT_1:49;
hence D1 . i is closed_interval Subset of REAL by A12, A13, A14; :: thesis:

end;

then consider r1 being Real, E1 being Element of Prod_Field (L-Field n) such that
A15: ( E1 = CarProduct D1 & (Prod_Measure (L-Meas n)) . E1 = r1 & 0 <= r1 ) by A11;
for i being Nat st i in Seg (n + 1) holds
D . i is Interval by A12;
then reconsider E = CarProduct D as Element of Prod_Field (L-Field (n + 1)) by Th9;
A16: D . (n + 1) is closed_interval Subset of REAL by A12, FINSEQ_1:4;
then reconsider E2 = D . (n + 1) as Element of L-Field by MEASUR12:72, MEASUR12:75;
consider a, b being Real such that
A17: D . (n + 1) = [.a,b.] by A16, MEASURE5:def 3;
CarProduct D = [:(CarProduct D1),(D . (n + 1)):] by Th4;
then A18: (Prod_Measure (L-Meas (n + 1))) . E = ((Prod_Measure (L-Meas n)) . E1) * (L-Meas . E2) by A15, Th51;

per cases ;

suppose D . (n + 1) = {} ; :: thesis:

then A19: L-Meas . E2 = 0 by VALUED_0:def 19;
take r = 0 ; :: thesis:
take E ; :: thesis:
thus E = CarProduct D ; :: thesis:
thus (Prod_Measure (L-Meas (n + 1))) . E = r by A18, A19; :: thesis:
thus 0 <= r ; :: thesis:

end;

suppose A20: D . (n + 1) <> {} ; :: thesis:

then a <= b by A17, XXREAL_1:29;
then A21: L-Meas . E2 = b - a by A17, MESFUN14:5;
take r = r1 * (b - a); :: thesis:
take E ; :: thesis:
thus E = CarProduct D ; :: thesis:
thus (Prod_Measure (L-Meas (n + 1))) . E = r by A18, A15, A21, XXREAL_3:def 5; :: thesis:
b - a >= 0 by A17, A20, XREAL_1:48, XXREAL_1:29;
hence 0 <= r by A15; :: thesis:

end;

end;

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A1, A10);
hence for D being n -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) holds
ex r being Real ex E being Element of Prod_Field (L-Field n) st
( E = CarProduct D & (Prod_Measure (L-Meas n)) . E = r & 0 <= r ) ; :: thesis: