let n be non zero Nat; :: thesis: for D being n -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | (CarProduct D) holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2)
let D be n -element FinSequence; :: thesis: for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | (CarProduct D) holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2)
let I be Subset of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | (CarProduct D) holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2)
let J be closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | (CarProduct D) holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2)
let f be PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | (CarProduct D) holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2)
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for G2 being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | (CarProduct D) holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2)
let G2 be PartFunc of (CarProduct ((Seg n) --> REAL)),REAL; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | (CarProduct D) implies Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2) )
assume that
A1: for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL and
A2: I = CarProduct D and
A3: [:I,J:] = dom f and
A4: f is_continuous_on [:I,J:] and
A5: f = g and
A6: G2 = (Integral2 (L-Meas,(R_EAL g))) | (CarProduct D) ; :: thesis: Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2)
set Rg = R_EAL g;
set RG2 = Integral2 (L-Meas,(R_EAL g));
for i being Nat st i in Seg n holds
D . i is Subset of REAL by A1;
then reconsider I0 = CarProduct D as Subset of (CarProduct ((Seg n) --> REAL)) by FINSEQ_1:3, Th11;
set NI = (CarProduct ((Seg n) --> REAL)) \ I0;
reconsider F0 = (Integral2 (L-Meas,(R_EAL g))) | I0, F1 = (Integral2 (L-Meas,(R_EAL g))) | ((CarProduct ((Seg n) --> REAL)) \ I0) as PartFunc of (CarProduct ((Seg n) --> REAL)),ExtREAL by PARTFUN1:11;
reconsider GG2 = G2 as PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real by MEASUR15:42;
A7: dom (Integral2 (L-Meas,(R_EAL g))) = CarProduct ((Seg n) --> REAL) by FUNCT_2:def 1;
for i being Nat st i in Seg n holds
D . i is Interval by A1;
then A8: I0 is Element of Prod_Field (L-Field n) by Th9;
CarProduct ((Seg n) --> REAL) in Prod_Field (L-Field n) by PROB_1:5;
then A9: (CarProduct ((Seg n) --> REAL)) \ I0 is Element of Prod_Field (L-Field n) by A8, PROB_1:6;
A10: Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,(R_EAL g)))) by A1, A2, A4, A3, A5, Lm3;
I0 \/ ((CarProduct ((Seg n) --> REAL)) \ I0) = CarProduct ((Seg n) --> REAL) by XBOOLE_1:45;
then A11: (Integral2 (L-Meas,(R_EAL g))) | (I0 \/ ((CarProduct ((Seg n) --> REAL)) \ I0)) = Integral2 (L-Meas,(R_EAL g)) ;
A12: F0 = R_EAL G2 by A6, MESFUNC5:def 7;
Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas n) by A1, A2, A4, A5, A3, Lm3;
then A13: Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,(R_EAL g)))) = (Integral ((Prod_Measure (L-Meas n)),F0)) + (Integral ((Prod_Measure (L-Meas n)),F1)) by A8, A9, A11, XBOOLE_1:85, MESFUNC5:98;
for x being Element of CarProduct ((Seg n) --> REAL) st x in dom F1 holds
F1 . x = 0

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis: ( x in dom F1 implies F1 . x = 0 )
assume A14: x in dom F1 ; :: thesis: F1 . x = 0
then not x in I0 by A7, XBOOLE_0:def 5;
then A15: dom (ProjPMap1 ((R_EAL g),x)) = {} by A2, A3, A5, MESFUN16:27;
(Integral2 (L-Meas,(R_EAL g))) . x = Integral (L-Meas,(ProjPMap1 ((R_EAL g),x))) by MESFUN12:def 8;
then (Integral2 (L-Meas,(R_EAL g))) . x = 0 by A15, MESFUN16:1;
hence F1 . x = 0 by A7, A14, FUNCT_1:49; :: thesis: verum

end;

then Integral ((Prod_Measure (L-Meas n)),F1) = 0 by A9, A7, MESFUN12:57;
hence Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2) by A12, A10, A13, XXREAL_3:4; :: thesis: verum