let I, J, K be non empty closed_interval Subset of REAL; 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
( ( for y being Element of REAL holds (Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty ) & ( for y being Element of REAL holds ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is_integrable_on L-Meas ) )
let f be 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
( ( for y being Element of REAL holds (Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty ) & ( for y being Element of REAL holds ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is_integrable_on L-Meas ) )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g implies ( ( for y being Element of REAL holds (Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty ) & ( for y being Element of REAL holds ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is_integrable_on L-Meas ) ) )
assume that
A1:
[:[:I,J:],K:] = dom f
and
A2:
f is_continuous_on [:[:I,J:],K:]
and
A3:
f = g
; ( ( for y being Element of REAL holds (Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty ) & ( for y being Element of REAL holds ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is_integrable_on L-Meas ) )
A4:
dom (R_EAL g) = [:[:I,J:],K:]
by A1, A3, MESFUNC5:def 7;
A5:
[#] REAL = REAL
by SUBSET_1:def 3;
A6:
REAL in L-Field
by PROB_1:5;
set Fz = Integral2 (L-Meas,(R_EAL g));
reconsider Gz = Integral2 (L-Meas,(R_EAL g)) as Function of [:REAL,REAL:],REAL by A1, A2, A3, Th32;
reconsider G = Gz | [:I,J:] as PartFunc of [:REAL,REAL:],REAL ;
reconsider F = G as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A7:
dom Gz = [:REAL,REAL:]
by FUNCT_2:def 1;
F is_uniformly_continuous_on [:I,J:]
by A1, A2, A3, Th34;
then A8:
F is_continuous_on [:I,J:]
by NFCONT_2:7;
thus A9:
for y being Element of REAL holds (Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty
for y being Element of REAL holds ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is_integrable_on L-Meas proof
let y be
Element of
REAL ;
(Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty
dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:]
by FUNCT_2:def 1;
then
dom |.(Integral2 (L-Meas,(R_EAL g))).| = [:REAL,REAL:]
by MESFUNC1:def 10;
then A10:
dom (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) = REAL
by A5, MESFUN16:26;
per cases
( y in J or not y in J )
;
suppose A11:
y in J
;
(Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty A12:
I misses REAL \ I
by XBOOLE_1:79;
A13:
I is
Element of
L-Field
by MEASUR10:5, MEASUR12:75;
REAL in L-Field
by PROB_1:5;
then reconsider NI =
REAL \ I as
Element of
L-Field by A13, PROB_1:6;
A14:
I \/ NI = REAL
by XBOOLE_1:45;
set Fz2 =
ProjPMap2 (
|.(Integral2 (L-Meas,(R_EAL g))).|,
y);
set L0 =
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I;
set L1 =
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI;
A16:
now for x being Element of REAL st x in dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) holds
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = 0 let x be
Element of
REAL ;
( x in dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) implies ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = 0 )assume A17:
x in dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI)
;
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = 0 then A18:
(
x in REAL & not
x in I )
by XBOOLE_0:def 5;
[x,y] in [:REAL,REAL:]
;
then
[x,y] in dom (Integral2 (L-Meas,(R_EAL g)))
by FUNCT_2:def 1;
then A19:
[x,y] in dom |.(Integral2 (L-Meas,(R_EAL g))).|
by MESFUNC1:def 10;
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . x
by A17, FUNCT_1:49;
then
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = |.(Integral2 (L-Meas,(R_EAL g))).| . (
x,
y)
by A19, MESFUN12:def 4;
then A20:
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = |.((Integral2 (L-Meas,(R_EAL g))) . (x,y)).|
by A19, MESFUNC1:def 10;
A21:
(Integral2 (L-Meas,(R_EAL g))) . (
x,
y)
= Integral (
L-Meas,
(ProjPMap1 ((R_EAL g),[x,y])))
by MESFUN12:def 8;
not
[x,y] in [:I,J:]
by A18, ZFMISC_1:87;
then
dom (ProjPMap1 ((R_EAL g),[x,y])) = {}
by A4, MESFUN16:25;
hence
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = 0
by A20, A21, EXTREAL1:16, MESFUN16:1;
verum end; then A22:
Integral (
L-Meas,
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI))
= 0
by A10, MESFUN12:57;
A23:
for
t being
Element of
REAL st
t in I holds
0 <= ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . t
proof
let t be
Element of
REAL ;
( t in I implies 0 <= ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . t )
assume A24:
t in I
;
0 <= ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . t
[t,y] in [:REAL,REAL:]
;
then
[t,y] in dom (Integral2 (L-Meas,(R_EAL g)))
by FUNCT_2:def 1;
then A25:
[t,y] in dom |.(Integral2 (L-Meas,(R_EAL g))).|
by MESFUNC1:def 10;
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . t = (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . t
by FUNCT_1:49, A24;
then
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . t = |.(Integral2 (L-Meas,(R_EAL g))).| . (
t,
y)
by A25, MESFUN12:def 4;
then
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . t = |.((Integral2 (L-Meas,(R_EAL g))) . (t,y)).|
by A25, MESFUNC1:def 10;
hence
0 <= ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . t
by EXTREAL1:14;
verum
end;
Integral2 (
L-Meas,
(R_EAL g))
= R_EAL Gz
by MESFUNC5:def 7;
then A26:
|.(Integral2 (L-Meas,(R_EAL g))).| = R_EAL |.Gz.|
by MESFUNC6:44;
then A27:
|.(Integral2 (L-Meas,(R_EAL g))).| = |.Gz.|
by MESFUNC5:def 7;
reconsider AFz =
|.(Integral2 (L-Meas,(R_EAL g))).| as
PartFunc of
[:REAL,REAL:],
REAL by A26, MESFUNC5:def 7;
R_EAL AFz = |.(Integral2 (L-Meas,(R_EAL g))).|
by MESFUNC5:def 7;
then
R_EAL (ProjPMap2 (AFz,y)) = ProjPMap2 (
|.(Integral2 (L-Meas,(R_EAL g))).|,
y)
by MESFUN16:31;
then
ProjPMap2 (
AFz,
y)
= ProjPMap2 (
|.(Integral2 (L-Meas,(R_EAL g))).|,
y)
by MESFUNC5:def 7;
then reconsider Gz2 =
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I as
PartFunc of
REAL,
REAL by PARTFUN1:11;
A28:
ProjPMap2 (
|.G.|,
y) is
continuous
by A7, A8, MESFUN16:34;
A29:
I is
Element of
L-Field
by MEASUR10:5, MEASUR12:75;
A30:
dom Gz2 = I
by A10;
I = Y-section (
[:I,J:],
y)
by A11, MEASUR11:22;
then A31:
Gz2 = ProjPMap2 (
(|.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:]),
y)
by MESFUN12:34;
|.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:] = |.G.|
by A27, RFUNCT_1:46;
then
|.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:] = R_EAL |.G.|
by MESFUNC5:def 7;
then
Gz2 = R_EAL (ProjPMap2 (|.G.|,y))
by A31, MESFUN16:31;
then
Gz2 is
continuous
by A28, MESFUNC5:def 7;
then
(
Gz2 || I is
bounded &
Gz2 is_integrable_on I )
by A10, INTEGRA5:10, INTEGRA5:11;
then
Gz2 is_integrable_on L-Meas
by A29, A30, MESFUN14:49;
then
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I is_integrable_on L-Meas
by MESFUNC5:def 7;
then A32:
Integral (
L-Meas,
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I))
< +infty
by MESFUNC5:96;
A33:
for
r being
Element of
REAL holds
0. <= (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . r
reconsider H =
REAL as
Element of
L-Field by PROB_1:5;
A36:
ProjPMap2 (
|.(Integral2 (L-Meas,(R_EAL g))).|,
y) is
H -measurable
by A1, A2, A3, A11, Th47;
A37:
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | (I \/ NI) = ProjPMap2 (
|.(Integral2 (L-Meas,(R_EAL g))).|,
y)
by A14;
Integral (
L-Meas,
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)))
= (Integral (L-Meas,((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I))) + (Integral (L-Meas,((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI)))
by A10, A13, A33, A36, A12, A37, SUPINF_2:39, MESFUNC5:91;
then
Integral (
L-Meas,
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I))
= Integral (
L-Meas,
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)))
by A22, XXREAL_3:4;
hence
(Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty
by A32, MESFUN12:def 7;
verum end; suppose A38:
not
y in J
;
(Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty now for x being Element of REAL st x in dom (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) holds
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . x = 0 let x be
Element of
REAL ;
( x in dom (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) implies (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . x = 0 )assume
x in dom (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y))
;
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . x = 0
[x,y] in [:REAL,REAL:]
;
then
[x,y] in dom (Integral2 (L-Meas,(R_EAL g)))
by FUNCT_2:def 1;
then A39:
[x,y] in dom |.(Integral2 (L-Meas,(R_EAL g))).|
by MESFUNC1:def 10;
then
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . x = |.(Integral2 (L-Meas,(R_EAL g))).| . (
x,
y)
by MESFUN12:def 4;
then A40:
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . x = |.((Integral2 (L-Meas,(R_EAL g))) . (x,y)).|
by A39, MESFUNC1:def 10;
A41:
(Integral2 (L-Meas,(R_EAL g))) . (
x,
y)
= Integral (
L-Meas,
(ProjPMap1 ((R_EAL g),[x,y])))
by MESFUN12:def 8;
not
[x,y] in [:I,J:]
by A38, ZFMISC_1:87;
then
dom (ProjPMap1 ((R_EAL g),[x,y])) = {}
by A4, MESFUN16:25;
hence
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . x = 0
by A40, A41, EXTREAL1:16, MESFUN16:1;
verum end; then
Integral (
L-Meas,
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)))
= 0
by A10, A6, MESFUN12:57;
then
(Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y = 0
by MESFUN12:def 7;
hence
(Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty
by XREAL_0:def 1, XXREAL_0:9;
verum
end;
Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas,L-Meas)
by A1, A2, A3, Th43;
hence
for y being Element of REAL holds ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is_integrable_on L-Meas
by A9, MESFUN13:33, MESFUN16:5; verum