let n be non zero Nat; :: thesis: for D being n + 1 -element FinSequence
for f being PartFunc of (CarProduct ((Seg (n + 1)) --> RNS_Real)),RNS_Real
for g being PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL
for g0 being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st f = g & g0 = 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
( Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),g) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0) )
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
for g0 being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st f = g & g0 = 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
( Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),g) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0) )
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
for g0 being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st f = g & g0 = 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
( Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),g) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0) )
let g be PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL; :: thesis: for g0 being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st f = g & g0 = 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
( Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),g) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0) )
let g0 be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: ( f = g & g0 = 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 ( Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),g) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0) ) )
assume that
A1: f = g and
A2: g0 = g and
A3: for i being Nat st i in Seg (n + 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: ( Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),g) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0) )
reconsider f0 = g0 as PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real by MEASUR15:42;
reconsider Dn = D | n as n -element FinSequence ;
A6: n < n + 1 by NAT_1:13;
A7: Seg n c= Seg (n + 1) by FINSEQ_3:18;
A8: for i being Nat st i in Seg n holds
Dn . i is closed_interval Subset of REAL

proof

let i be Nat; :: thesis: ( i in Seg n implies Dn . i is closed_interval Subset of REAL )
assume A9: i in Seg n ; :: thesis: Dn . i is closed_interval Subset of REAL
then Dn . i = D . i by FUNCT_1:49;
hence Dn . i is closed_interval Subset of REAL by A3, A9, A7; :: thesis: verum

end;

for i being Nat st i in Seg n holds
Dn . i is Subset of REAL by A8;
then CarProduct Dn is Subset of (CarProduct ((Seg n) --> REAL)) by FINSEQ_1:3, Th11;
then reconsider D0 = CarProduct Dn as Subset of (CarProduct ((Seg n) --> RNS_Real)) by MEASUR15:42;
reconsider D1 = D . (n + 1) as closed_interval Subset of REAL by A3, A6, FINSEQ_3:11;
A10: [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] = CarProduct ((Seg (n + 1)) --> RNS_Real) by MEASUR15:38;
CarProduct D = [:D0,D1:] by Th4;
hence Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) by A8, A1, A2, A5, A4, A10, Lm3; :: thesis: Integral ((Prod_Measure (L-Meas (n + 1))),g) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0)
A11: [:(CarProduct ((Seg n) --> REAL)),REAL:] = CarProduct ((Seg (n + 1)) --> REAL) by MEASUR15:38;
Prod_Field (L-Field (n + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by MEASUR14:44;
hence Integral ((Prod_Measure (L-Meas (n + 1))),g) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0) by A2, A11, MEASUR14:48; :: thesis: verum