let n be non zero Nat; :: thesis: for I being Subset of (CarProduct ((Seg n) --> 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 st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( Integral2 (L-Meas,|.(R_EAL g).|) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL & Integral2 (L-Meas,(R_EAL g)) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL )
let I be Subset of (CarProduct ((Seg n) --> 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 st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( Integral2 (L-Meas,|.(R_EAL g).|) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL & Integral2 (L-Meas,(R_EAL g)) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL )
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 st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( Integral2 (L-Meas,|.(R_EAL g).|) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL & Integral2 (L-Meas,(R_EAL g)) is PartFunc of (CarProduct ((Seg n) --> 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 [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( Integral2 (L-Meas,|.(R_EAL g).|) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL & Integral2 (L-Meas,(R_EAL g)) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL )
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: ( [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g implies ( Integral2 (L-Meas,|.(R_EAL g).|) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL & Integral2 (L-Meas,(R_EAL g)) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL ) )
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g ; :: thesis: ( Integral2 (L-Meas,|.(R_EAL g).|) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL & Integral2 (L-Meas,(R_EAL g)) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL )
set Rg = R_EAL g;
set F = Integral2 (L-Meas,|.(R_EAL g).|);
A4: dom (Integral2 (L-Meas,|.(R_EAL g).|)) = CarProduct ((Seg n) --> REAL) by FUNCT_2:def 1;

now :: thesis: for y being object st y in rng (Integral2 (L-Meas,|.(R_EAL g).|)) holds
y in REAL

let y be object ; :: thesis: ( y in rng (Integral2 (L-Meas,|.(R_EAL g).|)) implies b₁ in REAL )
assume y in rng (Integral2 (L-Meas,|.(R_EAL g).|)) ; :: thesis: b₁ in REAL
then consider x being Element of CarProduct ((Seg n) --> REAL) such that
A5: ( x in dom (Integral2 (L-Meas,|.(R_EAL g).|)) & y = (Integral2 (L-Meas,|.(R_EAL g).|)) . x ) by PARTFUN1:3;
reconsider Pg = ProjPMap1 (|.(R_EAL g).|,x) as PartFunc of REAL,REAL by MESFUN16:30;

per cases ( x in I or not x in I ) ;

suppose A6: x in I ; :: thesis: b₁ in REAL

then A7: dom Pg = J by A1, A3, MESFUN16:27;

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

suppose J <> {} ; :: thesis: b₁ in REAL

then reconsider J = J as non empty closed_interval Subset of REAL ;
(Integral2 (L-Meas,|.(R_EAL g).|)) . x = integral (Pg,J) by A1, A2, A3, A6, Th32;
hence y in REAL by A5, XREAL_0:def 1; :: thesis: verum

end;

suppose J = {} ; :: thesis: b₁ in REAL

then Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,x))) = 0 by A7, MESFUN16:1;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . x = 0 by MESFUN12:def 8;
hence y in REAL by A5, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

suppose not x in I ; :: thesis: b₁ in REAL

then dom Pg = {} by A1, A3, MESFUN16:27;
then Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,x))) = 0 by MESFUN16:1;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . x = 0 by MESFUN12:def 8;
hence y in REAL by A5, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

then rng (Integral2 (L-Meas,|.(R_EAL g).|)) c= REAL ;
hence Integral2 (L-Meas,|.(R_EAL g).|) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL by A4, RELSET_1:4; :: thesis: Integral2 (L-Meas,(R_EAL g)) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL
set G = Integral2 (L-Meas,(R_EAL g));

now :: thesis: for y being object st y in rng (Integral2 (L-Meas,(R_EAL g))) holds
y in REAL

let y be object ; :: thesis: ( y in rng (Integral2 (L-Meas,(R_EAL g))) implies b₁ in REAL )
assume y in rng (Integral2 (L-Meas,(R_EAL g))) ; :: thesis: b₁ in REAL
then consider x being Element of CarProduct ((Seg n) --> REAL) such that
A8: ( x in dom (Integral2 (L-Meas,(R_EAL g))) & y = (Integral2 (L-Meas,(R_EAL g))) . x ) by PARTFUN1:3;
reconsider Pg = ProjPMap1 ((R_EAL g),x) as PartFunc of REAL,REAL by MESFUN16:30;

per cases ( x in I or not x in I ) ;

suppose A9: x in I ; :: thesis: b₁ in REAL

then A10: dom Pg = J by A1, A3, MESFUN16:27;

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

suppose J <> {} ; :: thesis: b₁ in REAL

then reconsider J = J as non empty closed_interval Subset of REAL ;
(Integral2 (L-Meas,(R_EAL g))) . x = integral (Pg,J) by A9, A1, A2, A3, Th30;
hence y in REAL by A8, XREAL_0:def 1; :: thesis: verum

end;

suppose J = {} ; :: thesis: b₁ in REAL

then Integral (L-Meas,(ProjPMap1 ((R_EAL g),x))) = 0 by A10, MESFUN16:1;
then (Integral2 (L-Meas,(R_EAL g))) . x = 0 by MESFUN12:def 8;
hence y in REAL by A8, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

suppose not x in I ; :: thesis: b₁ in REAL

then dom Pg = {} by A1, A3, MESFUN16:27;
then Integral (L-Meas,(ProjPMap1 ((R_EAL g),x))) = 0 by MESFUN16:1;
then (Integral2 (L-Meas,(R_EAL g))) . x = 0 by MESFUN12:def 8;
hence y in REAL by A8, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

then ( rng (Integral2 (L-Meas,(R_EAL g))) c= REAL & dom (Integral2 (L-Meas,(R_EAL g))) c= CarProduct ((Seg n) --> REAL) ) ;
hence Integral2 (L-Meas,(R_EAL g)) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL by RELSET_1:4; :: thesis: verum