let I, J, K be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K is PartFunc of REAL,REAL & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K is PartFunc of REAL,REAL )
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K is PartFunc of REAL,REAL & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K is PartFunc of REAL,REAL )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g implies ( Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K is PartFunc of REAL,REAL & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K is PartFunc of REAL,REAL ) )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g ; :: thesis: ( Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K is PartFunc of REAL,REAL & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K is PartFunc of REAL,REAL )
set F = Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|);
set RF = Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g));
A4: dom (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) = REAL by FUNCT_2:def 1;
A5: dom (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) = REAL by FUNCT_2:def 1;

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

let q be object ; :: thesis: ( q in rng (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) implies b₁ in REAL )
assume q in rng (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) ; :: thesis: b₁ in REAL
then consider z being Element of REAL such that
A6: ( z in dom (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) & q = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z ) by PARTFUN1:3;
reconsider Pg = ProjPMap2 (|.(R_EAL g).|,z) as PartFunc of [:REAL,REAL:],REAL by MESFUN16:30;
reconsider Pf = Pg as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;

per cases ( z in K or not z in K ) ;

suppose A7: z in K ; :: thesis: b₁ in REAL

then A8: dom Pf = [:I,J:] by A1, A3, MESFUN16:28;
then Pf is_continuous_on [:I,J:] by A1, A2, A3, Th20;
then reconsider G2 = (Integral2 (L-Meas,(R_EAL Pg))) | I as PartFunc of REAL,REAL by A8, MESFUN16:51;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg) by A1, A2, A3, A7, Th28
.= integral (G2,I) by A1, A2, A3, A8, Th20, MESFUN16:58 ;
hence q in REAL by A6, XREAL_0:def 1; :: thesis: verum

end;

suppose not z in K ; :: thesis: b₁ in REAL

then dom (ProjPMap2 (|.(R_EAL g).|,z)) = {} by A1, A3, MESFUN16:28;
then Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) = 0 by MESFUN16:1;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = 0 by MESFUN12:def 7;
hence q in REAL by A6, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

then rng (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) c= REAL ;
hence Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is Function of REAL,REAL by A4, RELSET_1:4; :: thesis: ( (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K is PartFunc of REAL,REAL & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K is PartFunc of REAL,REAL )
hence (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K is PartFunc of REAL,REAL by PARTFUN1:11; :: thesis: ( Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K is PartFunc of REAL,REAL )

now :: thesis: for q being object st q in rng (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) holds
q in REAL

let q be object ; :: thesis: ( q in rng (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) implies b₁ in REAL )
assume q in rng (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) ; :: thesis: b₁ in REAL
then consider z being Element of REAL such that
A9: ( z in dom (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) & q = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z ) by PARTFUN1:3;
reconsider Pg = ProjPMap2 ((R_EAL g),z) as PartFunc of [:REAL,REAL:],REAL by MESFUN16:30;
reconsider Pf = Pg as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;

per cases ( z in K or not z in K ) ;

suppose A10: z in K ; :: thesis: b₁ in REAL

then A11: dom Pf = [:I,J:] by A1, A3, MESFUN16:28;
then Pf is_continuous_on [:I,J:] by A1, A2, A3, Th18;
then reconsider G2 = (Integral2 (L-Meas,(R_EAL Pg))) | I as PartFunc of REAL,REAL by A11, MESFUN16:51;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg) by A1, A2, A3, A10, Th23
.= integral (G2,I) by A1, A2, A3, A11, Th18, MESFUN16:58 ;
hence q in REAL by A9, XREAL_0:def 1; :: thesis: verum

end;

suppose not z in K ; :: thesis: b₁ in REAL

then dom (ProjPMap2 ((R_EAL g),z)) = {} by A1, A3, MESFUN16:28;
then Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 ((R_EAL g),z))) = 0 by MESFUN16:1;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0 by MESFUN12:def 7;
hence q in REAL by A9, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

then rng (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) c= REAL ;
hence Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is Function of REAL,REAL by A5, RELSET_1:4; :: thesis: (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K is PartFunc of REAL,REAL
hence (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K is PartFunc of REAL,REAL by PARTFUN1:11; :: thesis: verum