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
for y being Element of REAL
for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & y in J holds
ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is E -measurable
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for y being Element of REAL
for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & y in J holds
ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is E -measurable
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; for y being Element of REAL
for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & y in J holds
ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is E -measurable
let y be Element of REAL ; for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & y in J holds
ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is E -measurable
let E be Element of L-Field ; ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & y in J implies ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is E -measurable )
assume that
A1:
[:[:I,J:],K:] = dom f
and
A2:
f is_continuous_on [:[:I,J:],K:]
and
A3:
f = g
and
A4:
y in J
; ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is E -measurable
A5:
dom (R_EAL g) = [:[:I,J:],K:]
by A1, A3, MESFUNC5:def 7;
A6:
[#] REAL = REAL
by SUBSET_1:def 3;
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;
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 A9:
dom (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) = REAL
by A6, MESFUN16:26;
A10:
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 A10, PROB_1:6;
A11:
I \/ NI = REAL
by XBOOLE_1:45;
A12:
I /\ NI = {}
by XBOOLE_1:85, XBOOLE_0:def 7;
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;
A13:
dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) = I
by A9;
A14:
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 A15:
x in dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI)
;
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = 0 then A16:
(
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 A17:
[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 A15, FUNCT_1:49;
then
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = |.(Integral2 (L-Meas,(R_EAL g))).| . (
x,
y)
by A17, MESFUN12:def 4;
then A18:
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = |.((Integral2 (L-Meas,(R_EAL g))) . (x,y)).|
by A17, MESFUNC1:def 10;
A19:
(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 A16, ZFMISC_1:87;
then
dom (ProjPMap1 ((R_EAL g),[x,y])) = {}
by A5, MESFUN16:25;
hence
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . x = 0
by A18, A19, EXTREAL1:16, MESFUN16:1;
verum end;
A20:
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 A21:
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 A22:
[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, A21;
then
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . t = |.(Integral2 (L-Meas,(R_EAL g))).| . (
t,
y)
by A22, MESFUN12:def 4;
then
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . t = |.((Integral2 (L-Meas,(R_EAL g))) . (t,y)).|
by A22, 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 A23:
|.(Integral2 (L-Meas,(R_EAL g))).| = R_EAL |.Gz.|
by MESFUNC6:44;
then A24:
|.(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 A23, 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;
A25:
ProjPMap2 (|.G.|,y) is continuous
by A7, A8, MESFUN16:34;
A26:
I is Element of L-Field
by MEASUR10:5, MEASUR12:75;
A27:
dom Gz2 = I
by A9;
I = Y-section ([:I,J:],y)
by A4, MEASUR11:22;
then A28:
Gz2 = ProjPMap2 ((|.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:]),y)
by MESFUN12:34;
|.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:] = |.G.|
by A24, 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 A28, MESFUN16:31;
then
Gz2 is continuous
by A25, MESFUNC5:def 7;
then
( Gz2 || I is bounded & Gz2 is_integrable_on I )
by A9, INTEGRA5:10, INTEGRA5:11;
then
Gz2 is_integrable_on L-Meas
by A26, A27, MESFUN14:49;
then A29:
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I is_integrable_on L-Meas
by MESFUNC5:def 7;
A30:
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;
for r being Real holds H /\ (less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)) in L-Field
proof
let r be
Real;
H /\ (less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)) in L-Field
consider H0 being
Element of
L-Field such that A33:
(
H0 = dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) &
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I is
H0 -measurable )
by A29, MESFUNC5:def 17;
per cases
( r <= 0 or 0 < r )
;
suppose A34:
r <= 0
;
H /\ (less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)) in L-Field
less_dom (
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),
r)
= {}
proof
assume
less_dom (
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),
r)
<> {}
;
contradiction
then consider y being
object such that A35:
y in less_dom (
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),
r)
by XBOOLE_0:def 1;
(
y in dom (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) &
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . y < r )
by MESFUNC1:def 11, A35;
hence
contradiction
by A30, A34;
verum
end; hence
H /\ (less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)) in L-Field
by PROB_1:4;
verum end; suppose A36:
0 < r
;
H /\ (less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)) in L-Field A37:
for
z being
object holds
(
z in less_dom (
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),
r) iff
z in (less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI )
proof
let z be
object ;
( z in less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r) iff z in (less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI )
hereby ( z in (less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI implies z in less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r) )
assume A38:
z in less_dom (
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),
r)
;
z in (less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NIthen A39:
(
z in dom (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) &
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . z < r )
by MESFUNC1:def 11;
per cases
( z in I or z in NI )
by A38, A11, XBOOLE_0:def 3;
suppose A40:
z in I
;
z in (less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NIthen
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . z < r
by FUNCT_1:49, A39;
then
z in less_dom (
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),
r)
by A13, A40, MESFUNC1:def 11;
hence
z in (less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI
by XBOOLE_0:def 3;
verum end;
end;
assume
z in (less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI
;
z in less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)
per cases then
( z in less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r) or z in NI )
by XBOOLE_0:def 3;
suppose A41:
z in less_dom (
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),
r)
;
z in less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)then
(
z in dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) &
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I) . z < r )
by MESFUNC1:def 11;
then
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . z < r
by FUNCT_1:49;
hence
z in less_dom (
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),
r)
by A9, A41, MESFUNC1:def 11;
verum end; suppose A42:
z in NI
;
z in less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)then reconsider u =
z as
Element of
REAL ;
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . u = ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | NI) . z
by A42, FUNCT_1:49;
then
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . u = 0
by A14, A42, A9;
hence
z in less_dom (
(ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),
r)
by A9, A36, MESFUNC1:def 11;
verum end;
end; A43:
H /\ (less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)) =
(I \/ NI) /\ (less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r))
by XBOOLE_1:45
.=
(I \/ NI) /\ ((less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI)
by A37, TARSKI:2
.=
(I /\ ((less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI)) \/ (NI /\ ((less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI))
by XBOOLE_1:23
;
I /\ ((less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI) = (I /\ (less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r))) \/ {}
by A12, XBOOLE_1:23;
then A44:
I /\ ((less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI) in L-Field
by A9, A33;
A45:
less_dom (
((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),
r)
c= I
by A13, MESFUNC1:def 11;
NI /\ ((less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI) = (NI /\ (less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r))) \/ (NI /\ NI)
by XBOOLE_1:23;
then
NI /\ ((less_dom (((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) | I),r)) \/ NI) = {} \/ (NI /\ NI)
by A45;
hence
H /\ (less_dom ((ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)),r)) in L-Field
by A43, A44, PROB_1:3;
verum end;
end;
then
ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is H -measurable
;
hence
ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is E -measurable
by MESFUNC1:30; verum