let n be non zero Nat; :: thesis: for D being n -element FinSequence
for J being 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 st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g holds
( (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J is PartFunc of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J is PartFunc of REAL,REAL )
let D be n -element FinSequence; :: thesis: for J being 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 st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g holds
( (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J is PartFunc of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J is PartFunc of REAL,REAL )
let J be 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 st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g holds
( (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J is PartFunc of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J is PartFunc of REAL,REAL )
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 st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g holds
( (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J is PartFunc of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J is PartFunc of REAL,REAL )
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g implies ( (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J is PartFunc of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J is PartFunc of REAL,REAL ) )
assume that
A1: for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL and
A2: [:(CarProduct D),J:] = dom f and
A3: f is_continuous_on [:(CarProduct D),J:] and
A4: f = g ; :: thesis: ( (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J is PartFunc of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J is PartFunc of REAL,REAL )
set g1 = R_EAL g;
set T = Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|);
A5: dom (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) = REAL by FUNCT_2:def 1;
reconsider T0 = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J as PartFunc of REAL,ExtREAL by PARTFUN1:11;
set RT = Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g));
A6: dom (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) = REAL by FUNCT_2:def 1;
reconsider RT0 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J as PartFunc of REAL,ExtREAL by PARTFUN1:11;

now :: thesis: for x being object st x in rng T0 holds
x in REAL

let x be object ; :: thesis: ( x in rng T0 implies x in REAL )
assume x in rng T0 ; :: thesis: x in REAL
then consider y being Element of REAL such that
A7: ( y in dom T0 & x = T0 . y ) by PARTFUN1:3;
reconsider Pg = ProjPMap2 (|.(R_EAL g).|,y) as PartFunc of (CarProduct ((Seg n) --> REAL)),REAL by MESFUN16:30;
A8: R_EAL Pg = ProjPMap2 (|.(R_EAL g).|,y) by MESFUNC5:def 7;
Pg is_integrable_on Prod_Measure (L-Meas n) by A7, A1, A5, A2, A3, A4, Th48;
then ( -infty < Integral ((Prod_Measure (L-Meas n)),Pg) & Integral ((Prod_Measure (L-Meas n)),Pg) < +infty ) by MESFUNC6:90;
then A9: Integral ((Prod_Measure (L-Meas n)),Pg) in REAL by XXREAL_0:14;
(Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y = Integral ((Prod_Measure (L-Meas n)),Pg) by A8, A7, A1, A5, A2, A3, A4, Th48;
hence x in REAL by A7, A5, A9, FUNCT_1:49; :: thesis: verum

end;

then ( rng T0 c= REAL & dom T0 c= REAL ) ;
hence (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J is PartFunc of REAL,REAL by RELSET_1:4; :: thesis: (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J is PartFunc of REAL,REAL

now :: thesis: for x being object st x in rng RT0 holds
x in REAL

let x be object ; :: thesis: ( x in rng RT0 implies x in REAL )
assume x in rng RT0 ; :: thesis: x in REAL
then consider y being Element of REAL such that
A10: ( y in dom RT0 & x = RT0 . y ) by PARTFUN1:3;
reconsider Pg = ProjPMap2 ((R_EAL g),y) as PartFunc of (CarProduct ((Seg n) --> REAL)),REAL by MESFUN16:30;
A11: R_EAL Pg = ProjPMap2 ((R_EAL g),y) by MESFUNC5:def 7;
Pg is_integrable_on Prod_Measure (L-Meas n) by A1, A10, A6, A2, A3, A4, Th45;
then ( -infty < Integral ((Prod_Measure (L-Meas n)),Pg) & Integral ((Prod_Measure (L-Meas n)),Pg) < +infty ) by MESFUNC6:90;
then A12: Integral ((Prod_Measure (L-Meas n)),Pg) in REAL by XXREAL_0:14;
(Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) . y = Integral ((Prod_Measure (L-Meas n)),Pg) by A11, A1, A10, A6, A2, A3, A4, Th45;
hence x in REAL by A10, A6, A12, FUNCT_1:49; :: thesis: verum

end;

then ( rng RT0 c= REAL & dom RT0 c= REAL ) ;
hence (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J is PartFunc of REAL,REAL by RELSET_1:4; :: thesis: verum