let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for n being Nat
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = n holds
integral X,S,M,f = Sum x
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for n being Nat
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = n holds
integral X,S,M,f = Sum x
let M be sigma_Measure of S; :: thesis: for n being Nat
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = n holds
integral X,S,M,f = Sum x
defpred S1[ Nat] means for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = $1 holds
integral X,S,M,f = Sum x;
A1:
S1[ 0 ]
proof
let f be
PartFunc of
X,
ExtREAL ;
:: thesis: for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = 0 holds
integral X,S,M,f = Sum xlet F be
Finite_Sep_Sequence of
S;
:: thesis: for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = 0 holds
integral X,S,M,f = Sum xlet a,
x be
FinSequence of
ExtREAL ;
:: thesis: ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = 0 implies integral X,S,M,f = Sum x )
assume that
f is_simple_func_in S
and A2:
dom f <> {}
and
for
x being
set st
x in dom f holds
0. <= f . x
and A3:
F,
a are_Re-presentation_of f
and
dom x = dom F
and
for
i being
Nat st
i in dom x holds
x . i = (a . i) * ((M * F) . i)
and A4:
len F = 0
;
:: thesis: integral X,S,M,f = Sum x
dom F = {}
by A4, FINSEQ_1:4, FINSEQ_1:def 3;
then
union (rng F) = {}
by RELAT_1:65, ZFMISC_1:2;
hence
integral X,
S,
M,
f = Sum x
by A2, A3, MESFUNC3:def 1;
:: thesis: verum
end;
A5:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A6:
S1[
n]
;
:: thesis: S1[n + 1]
let f be
PartFunc of
X,
ExtREAL ;
:: thesis: for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = n + 1 holds
integral X,S,M,f = Sum xlet F be
Finite_Sep_Sequence of
S;
:: thesis: for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = n + 1 holds
integral X,S,M,f = Sum xlet a,
x be
FinSequence of
ExtREAL ;
:: thesis: ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = n + 1 implies integral X,S,M,f = Sum x )
assume that A7:
f is_simple_func_in S
and A8:
dom f <> {}
and A9:
for
x being
set st
x in dom f holds
0. <= f . x
and A10:
F,
a are_Re-presentation_of f
and A11:
dom x = dom F
and A12:
for
i being
Nat st
i in dom x holds
x . i = (a . i) * ((M * F) . i)
and A13:
len F = n + 1
;
:: thesis: integral X,S,M,f = Sum x
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
set F1 =
F | (Seg n);
set a1 =
a | (Seg n);
set x1 =
x | (Seg n);
set f1 =
f | (union (rng (F | (Seg n))));
reconsider F1 =
F | (Seg n) as
Finite_Sep_Sequence of
S by MESFUNC2:36;
reconsider a1 =
a | (Seg n) as
FinSequence of
ExtREAL by FINSEQ_1:23;
reconsider x1 =
x | (Seg n) as
FinSequence of
ExtREAL by FINSEQ_1:23;
A14:
f is
real-valued
by A7, MESFUNC2:def 5;
for
x being
Element of
X st
x in dom (f | (union (rng (F | (Seg n))))) holds
|.((f | (union (rng (F | (Seg n))))) . x).| < +infty
by A14, MESFUNC2:def 1;
then A17:
f | (union (rng (F | (Seg n)))) is
real-valued
by MESFUNC2:def 1;
A18:
dom (f | (union (rng (F | (Seg n))))) = union (rng F1)
A20:
f | (union (rng (F | (Seg n)))) is_simple_func_in S
A24:
for
x being
set st
x in dom (f | (union (rng (F | (Seg n))))) holds
0. <= (f | (union (rng (F | (Seg n))))) . x
A26:
dom F1 =
(dom F) /\ (Seg n)
by RELAT_1:90
.=
(dom a) /\ (Seg n)
by A10, MESFUNC3:def 1
.=
dom a1
by RELAT_1:90
;
for
n being
Nat st
n in dom F1 holds
for
x being
set st
x in F1 . n holds
(f | (union (rng (F | (Seg n))))) . x = a1 . n
then A30:
F1,
a1 are_Re-presentation_of f | (union (rng (F | (Seg n))))
by A18, A26, MESFUNC3:def 1;
A31:
dom x1 =
(dom F) /\ (Seg n)
by A11, RELAT_1:90
.=
dom F1
by RELAT_1:90
;
now per cases
( dom (f | (union (rng (F | (Seg n))))) = {} or dom (f | (union (rng (F | (Seg n))))) <> {} )
;
suppose A32:
dom (f | (union (rng (F | (Seg n))))) = {}
;
:: thesis: integral X,S,M,f = Sum xA33:
for
m being
Nat st
m in dom F1 holds
F1 . m = {}
A34:
for
m being
Nat st
m in dom F1 holds
x . m = 0.
consider sumx being
Function of
NAT ,
ExtREAL such that A39:
(
Sum x = sumx . (len x) &
sumx . 0 = 0. & ( for
m being
Element of
NAT st
m < len x holds
sumx . (m + 1) = (sumx . m) + (x . (m + 1)) ) )
by CONVFUN1:def 5;
A40:
Seg (len x) =
dom F
by A11, FINSEQ_1:def 3
.=
Seg (n + 1)
by A13, FINSEQ_1:def 3
;
then A41:
len x = n + 1
by FINSEQ_1:8;
defpred S2[
Nat]
means ( $1
< len x implies
sumx . $1
= 0. );
A42:
S2[
0 ]
by A39;
A43:
for
m being
Nat st
S2[
m] holds
S2[
m + 1]
proof
let m be
Nat;
:: thesis: ( S2[m] implies S2[m + 1] )
assume A44:
S2[
m]
;
:: thesis: S2[m + 1]
assume A45:
m + 1
< len x
;
:: thesis: sumx . (m + 1) = 0.
m <= m + 1
by NAT_1:11;
then A46:
m < len x
by A45, XXREAL_0:2;
A47:
( 1
<= m + 1 &
(m + 1) + 1
<= len x )
by A45, NAT_1:11, NAT_1:13;
then
m + 1
in Seg (len x)
by A45, FINSEQ_1:3;
then A48:
m + 1
in dom F
by A11, FINSEQ_1:def 3;
m + 1
<= n
by A41, A45, NAT_1:13;
then
m + 1
in Seg n
by A47, FINSEQ_1:3;
then
m + 1
in (dom F) /\ (Seg n)
by A48, XBOOLE_0:def 4;
then A49:
m + 1
in dom F1
by RELAT_1:90;
m in NAT
by ORDINAL1:def 13;
then sumx . (m + 1) =
0. + (x . (m + 1))
by A39, A44, A46
.=
x . (m + 1)
by XXREAL_3:4
;
hence
sumx . (m + 1) = 0.
by A34, A49;
:: thesis: verum
end; A50:
for
m being
Nat holds
S2[
m]
from NAT_1:sch 2(A42, A43);
A51:
n < len x
by A41, NAT_1:13;
A52:
Sum x =
sumx . (n + 1)
by A39, A40, FINSEQ_1:8
.=
(sumx . n) + (x . (n + 1))
by A39, A51
.=
0. + (x . (n + 1))
by A50, A51
.=
x . (n + 1)
by XXREAL_3:4
;
( 1
<= n + 1 &
n + 1
<= len F )
by A13, NAT_1:11;
then A53:
n + 1
in dom F
by FINSEQ_3:27;
A54:
union (rng F) = (union (rng F1)) \/ (F . (n + 1))
now per cases
( a . (n + 1) <> 0. or a . (n + 1) = 0. )
;
case A63:
a . (n + 1) <> 0.
;
:: thesis: integral X,S,M,f = Sum xdefpred S3[
Nat,
set ]
means ( ( $1
= 1 implies $2
= union (rng F1) ) & ( $1
= 2 implies $2
= F . (n + 1) ) );
A64:
for
k being
Nat st
k in Seg 2 holds
ex
x being
Element of
S st
S3[
k,
x]
consider G being
FinSequence of
S such that A68:
(
dom G = Seg 2 & ( for
k being
Nat st
k in Seg 2 holds
S3[
k,
G . k] ) )
from FINSEQ_1:sch 5(A64);
A69:
len G = 2
by A68, FINSEQ_1:def 3;
A70:
1
in Seg 2
by FINSEQ_1:4, TARSKI:def 2;
then A71:
G . 1
= union (rng F1)
by A68;
A72:
2
in Seg 2
by FINSEQ_1:4, TARSKI:def 2;
then A73:
G . 2
= F . (n + 1)
by A68;
then A74:
G = <*(union (rng F1)),(F . (n + 1))*>
by A69, A71, FINSEQ_1:61;
defpred S4[
Nat,
set ]
means ( ( $1
= 1 implies $2
= 0. ) & ( $1
= 2 implies $2
= a . (n + 1) ) );
A75:
for
k being
Nat st
k in Seg 2 holds
ex
x being
Element of
ExtREAL st
S4[
k,
x]
consider b being
FinSequence of
ExtREAL such that A79:
(
dom b = Seg 2 & ( for
k being
Nat st
k in Seg 2 holds
S4[
k,
b . k] ) )
from FINSEQ_1:sch 5(A75);
A80:
1
in Seg 2
by FINSEQ_1:4, TARSKI:def 2;
then A81:
b . 1
= 0.
by A79;
2
in Seg 2
by FINSEQ_1:4, TARSKI:def 2;
then A82:
b . 2
= a . (n + 1)
by A79;
deffunc H1(
Nat)
-> Element of
ExtREAL =
(b . $1) * ((M * G) . $1);
consider y being
FinSequence of
ExtREAL such that A83:
(
len y = 2 & ( for
m being
Nat st
m in dom y holds
y . m = H1(
m) ) )
from FINSEQ_2:sch 1();
A84:
dom y = Seg 2
by A83, FINSEQ_1:def 3;
1
in Seg 2
by FINSEQ_1:4, TARSKI:def 2;
then
y . 1
= (b . 1) * ((M * G) . 1)
by A83, A84;
then A85:
y . 1
= 0.
by A81;
A86:
y . 2
= x . (n + 1)
consider sumy being
Function of
NAT ,
ExtREAL such that A88:
(
Sum y = sumy . (len y) &
sumy . 0 = 0. & ( for
k being
Element of
NAT st
k < len y holds
sumy . (k + 1) = (sumy . k) + (y . (k + 1)) ) )
by CONVFUN1:def 5;
A89:
sumy . 1 =
(sumy . 0 ) + (y . (0 + 1))
by A83, A88
.=
0.
by A85, A88
;
A90:
Sum y =
sumy . (1 + 1)
by A83, A88
.=
0. + (x . (n + 1))
by A83, A86, A88, A89
.=
x . (n + 1)
by XXREAL_3:4
;
for
u,
v being
set st
u <> v holds
G . u misses G . v
proof
let u,
v be
set ;
:: thesis: ( u <> v implies G . u misses G . v )
assume A91:
u <> v
;
:: thesis: G . u misses G . v
per cases
( ( u in dom G & v in dom G ) or not u in dom G or not v in dom G )
;
suppose
(
u in dom G &
v in dom G )
;
:: thesis: G . u misses G . vthen A92:
( (
u = 1 or
u = 2 ) & (
v = 1 or
v = 2 ) )
by A68, FINSEQ_1:4, TARSKI:def 2;
per cases
( ( u = 1 & v = 2 ) or ( u = 2 & v = 1 ) )
by A91, A92;
suppose A93:
(
u = 1 &
v = 2 )
;
:: thesis: G . u misses G . vassume
G . u meets G . v
;
:: thesis: contradictionthen consider z being
set such that A94:
(
z in G . u &
z in G . v )
by XBOOLE_0:3;
consider A being
set such that A95:
(
z in A &
A in rng F1 )
by A71, A93, A94, TARSKI:def 4;
consider k' being
set such that A96:
(
k' in dom F1 &
A = F1 . k' )
by A95, FUNCT_1:def 5;
reconsider k' =
k' as
Element of
NAT by A96;
k' in (dom F) /\ (Seg n)
by A96, RELAT_1:90;
then
(
k' in dom F &
k' in Seg n )
by XBOOLE_0:def 4;
then
k' <= n
by FINSEQ_1:3;
then
k' < n + 1
by NAT_1:13;
then A97:
F . k' misses F . (n + 1)
by PROB_2:def 3;
(
z in F . k' &
z in F . (n + 1) )
by A68, A72, A93, A94, A95, A96, FUNCT_1:70;
hence
contradiction
by A97, XBOOLE_0:3;
:: thesis: verum end; suppose A98:
(
u = 2 &
v = 1 )
;
:: thesis: G . u misses G . vassume
G . u meets G . v
;
:: thesis: contradictionthen consider z being
set such that A99:
(
z in G . u &
z in G . v )
by XBOOLE_0:3;
consider A being
set such that A100:
(
z in A &
A in rng F1 )
by A71, A98, A99, TARSKI:def 4;
consider k' being
set such that A101:
(
k' in dom F1 &
A = F1 . k' )
by A100, FUNCT_1:def 5;
reconsider k' =
k' as
Element of
NAT by A101;
k' in (dom F) /\ (Seg n)
by A101, RELAT_1:90;
then
(
k' in dom F &
k' in Seg n )
by XBOOLE_0:def 4;
then
k' <= n
by FINSEQ_1:3;
then
k' < n + 1
by NAT_1:13;
then A102:
F . k' misses F . (n + 1)
by PROB_2:def 3;
(
z in F . k' &
z in F . (n + 1) )
by A68, A72, A98, A99, A100, A101, FUNCT_1:70;
hence
contradiction
by A102, XBOOLE_0:3;
:: thesis: verum end; end;
end; then reconsider G =
G as
Finite_Sep_Sequence of
S by PROB_2:def 3;
A103:
dom f =
(union (rng F1)) \/ (F . (n + 1))
by A10, A54, MESFUNC3:def 1
.=
union {(union (rng F1)),(F . (n + 1))}
by ZFMISC_1:93
.=
union (rng G)
by A74, FINSEQ_2:147
;
(
G,
b are_Re-presentation_of f &
b . 1
= 0. & ( for
m being
Nat st 2
<= m &
m in dom b holds
(
0. < b . m &
b . m < +infty ) ) &
dom y = dom G & ( for
m being
Nat st
m in dom y holds
y . m = (b . m) * ((M * G) . m) ) )
proof
A104:
for
k being
Nat st
k in dom G holds
for
v being
set st
v in G . k holds
f . v = b . k
hence
G,
b are_Re-presentation_of f
by A68, A79, A103, MESFUNC3:def 1;
:: thesis: ( b . 1 = 0. & ( for m being Nat st 2 <= m & m in dom b holds
( 0. < b . m & b . m < +infty ) ) & dom y = dom G & ( for m being Nat st m in dom y holds
y . m = (b . m) * ((M * G) . m) ) )
thus
b . 1
= 0.
by A79, A80;
:: thesis: ( ( for m being Nat st 2 <= m & m in dom b holds
( 0. < b . m & b . m < +infty ) ) & dom y = dom G & ( for m being Nat st m in dom y holds
y . m = (b . m) * ((M * G) . m) ) )
thus
for
k being
Nat st 2
<= k &
k in dom b holds
(
0. < b . k &
b . k < +infty )
:: thesis: ( dom y = dom G & ( for m being Nat st m in dom y holds
y . m = (b . m) * ((M * G) . m) ) )proof
let k be
Nat;
:: thesis: ( 2 <= k & k in dom b implies ( 0. < b . k & b . k < +infty ) )
assume A107:
( 2
<= k &
k in dom b )
;
:: thesis: ( 0. < b . k & b . k < +infty )
then A108:
(
k = 1 or
k = 2 )
by A79, FINSEQ_1:4, TARSKI:def 2;
then
G . k <> {}
by A8, A10, A18, A32, A54, A73, A107, MESFUNC3:def 1;
then consider v being
set such that A109:
v in G . k
by XBOOLE_0:def 1;
A110:
f . v = b . k
by A68, A79, A104, A107, A109;
A111:
v in dom f
by A10, A18, A32, A54, A73, A107, A108, A109, MESFUNC3:def 1;
hence
0. < b . k
by A9, A63, A82, A107, A108, A110;
:: thesis: b . k < +infty
dom f c= X
by RELAT_1:def 18;
then reconsider v =
v as
Element of
X by A111;
|.(f . v).| < +infty
by A14, A111, MESFUNC2:def 1;
hence
b . k < +infty
by A110, EXTREAL2:58;
:: thesis: verum
end;
thus
dom y = dom G
by A68, A83, FINSEQ_1:def 3;
:: thesis: for m being Nat st m in dom y holds
y . m = (b . m) * ((M * G) . m)
thus
for
m being
Nat st
m in dom y holds
y . m = (b . m) * ((M * G) . m)
by A83;
:: thesis: verum
end; hence
integral X,
S,
M,
f = Sum x
by A7, A8, A9, A52, A90, MESFUNC3:def 2;
:: thesis: verum end; case A112:
a . (n + 1) = 0.
;
:: thesis: integral X,S,M,f = Sum x
( 1
<= n + 1 &
n + 1
<= len x )
by A40, FINSEQ_1:8, NAT_1:11;
then
n + 1
in dom x
by FINSEQ_3:27;
then A113:
x . (n + 1) =
(a . (n + 1)) * ((M * F) . (n + 1))
by A12
.=
0.
by A112
;
defpred S3[
Nat,
set ]
means ( ( $1
= 1 implies $2
= union (rng F) ) & ( $1
= 2 implies $2
= {} ) );
A114:
for
k being
Nat st
k in Seg 2 holds
ex
v being
Element of
S st
S3[
k,
v]
consider G being
FinSequence of
S such that A118:
(
dom G = Seg 2 & ( for
k being
Nat st
k in Seg 2 holds
S3[
k,
G . k] ) )
from FINSEQ_1:sch 5(A114);
A119:
( 1
in Seg 2 & 2
in dom G & 2
in Seg 2 )
by A118, FINSEQ_1:4, TARSKI:def 2;
then A120:
(
G . 1
= union (rng F) &
G . 2
= {} &
M . (G . 2) = (M * G) . 2 )
by A118, FUNCT_1:23;
A121:
(M * G) . 2
= 0.
by A120, VALUED_0:def 19;
defpred S4[
Nat,
set ]
means ( ( $1
= 1 implies $2
= 0. ) & ( $1
= 2 implies $2
= 1. ) );
A122:
for
k being
Nat st
k in Seg 2 holds
ex
v being
Element of
ExtREAL st
S4[
k,
v]
consider b being
FinSequence of
ExtREAL such that A126:
(
dom b = Seg 2 & ( for
k being
Nat st
k in Seg 2 holds
S4[
k,
b . k] ) )
from FINSEQ_1:sch 5(A122);
A127:
( 1
in Seg 2 & 2
in Seg 2 )
by FINSEQ_1:4, TARSKI:def 2;
then A128:
(
b . 1
= 0. &
b . 2
= 1. )
by A126;
deffunc H1(
Nat)
-> Element of
ExtREAL =
(b . $1) * ((M * G) . $1);
consider y being
FinSequence of
ExtREAL such that A129:
(
len y = 2 & ( for
k being
Nat st
k in dom y holds
y . k = H1(
k) ) )
from FINSEQ_2:sch 1();
A130:
dom y = Seg 2
by A129, FINSEQ_1:def 3;
A131:
(
y . 1
= 0. &
y . 2
= 0. )
consider sumy being
Function of
NAT ,
ExtREAL such that A132:
(
Sum y = sumy . (len y) &
sumy . 0 = 0. & ( for
k being
Element of
NAT st
k < len y holds
sumy . (k + 1) = (sumy . k) + (y . (k + 1)) ) )
by CONVFUN1:def 5;
A133:
sumy . 1 =
(sumy . 0 ) + (y . (0 + 1))
by A129, A132
.=
0.
by A131, A132
;
A134:
Sum y =
(sumy . 1) + (y . (1 + 1))
by A129, A132
.=
0.
by A131, A133
;
for
u,
v being
set st
u <> v holds
G . u misses G . v
then reconsider G =
G as
Finite_Sep_Sequence of
S by PROB_2:def 3;
(
G,
b are_Re-presentation_of f &
b . 1
= 0. & ( for
m being
Nat st 2
<= m &
m in dom b holds
(
0. < b . m &
b . m < +infty ) ) &
dom y = dom G & ( for
m being
Nat st
m in dom y holds
y . m = (b . m) * ((M * G) . m) ) )
proof
len G = 2
by A118, FINSEQ_1:def 3;
then
G = <*(union (rng F)),{} *>
by A120, FINSEQ_1:61;
then
rng G = {(union (rng F)),{} }
by FINSEQ_2:147;
then A138:
union (rng G) =
(union (rng F)) \/ {}
by ZFMISC_1:93
.=
dom f
by A10, MESFUNC3:def 1
;
for
k being
Nat st
k in dom G holds
for
v being
set st
v in G . k holds
f . v = b . k
proof
let k be
Nat;
:: thesis: ( k in dom G implies for v being set st v in G . k holds
f . v = b . k )
assume A139:
k in dom G
;
:: thesis: for v being set st v in G . k holds
f . v = b . k
let v be
set ;
:: thesis: ( v in G . k implies f . v = b . k )
assume A140:
v in G . k
;
:: thesis: f . v = b . k
per cases
( k = 1 or k = 2 )
by A118, A139, FINSEQ_1:4, TARSKI:def 2;
suppose A141:
k = 1
;
:: thesis: f . v = b . kthen
f . v = 0.
by A10, A18, A32, A53, A54, A112, A120, A140, MESFUNC3:def 1;
hence
f . v = b . k
by A126, A127, A141;
:: thesis: verum end;
end;
hence
G,
b are_Re-presentation_of f
by A118, A126, A138, MESFUNC3:def 1;
:: thesis: ( b . 1 = 0. & ( for m being Nat st 2 <= m & m in dom b holds
( 0. < b . m & b . m < +infty ) ) & dom y = dom G & ( for m being Nat st m in dom y holds
y . m = (b . m) * ((M * G) . m) ) )
thus
b . 1
= 0.
by A126, A127;
:: thesis: ( ( for m being Nat st 2 <= m & m in dom b holds
( 0. < b . m & b . m < +infty ) ) & dom y = dom G & ( for m being Nat st m in dom y holds
y . m = (b . m) * ((M * G) . m) ) )
thus
for
k being
Nat st 2
<= k &
k in dom b holds
(
0. < b . k &
b . k < +infty )
:: thesis: ( dom y = dom G & ( for m being Nat st m in dom y holds
y . m = (b . m) * ((M * G) . m) ) )
thus
dom y = dom G
by A118, A129, FINSEQ_1:def 3;
:: thesis: for m being Nat st m in dom y holds
y . m = (b . m) * ((M * G) . m)
thus
for
m being
Nat st
m in dom y holds
y . m = (b . m) * ((M * G) . m)
by A129;
:: thesis: verum
end; hence
integral X,
S,
M,
f = Sum x
by A7, A8, A9, A52, A113, A134, MESFUNC3:def 2;
:: thesis: verum hence
integral X,
S,
M,
f = Sum x
;
:: thesis: verum end; suppose A142:
dom (f | (union (rng (F | (Seg n))))) <> {}
;
:: thesis: integral X,S,M,f = Sum xA143:
for
i being
Nat st
i in dom x1 holds
x1 . i = (a1 . i) * ((M * F1) . i)
proof
let i be
Nat;
:: thesis: ( i in dom x1 implies x1 . i = (a1 . i) * ((M * F1) . i) )
assume A144:
i in dom x1
;
:: thesis: x1 . i = (a1 . i) * ((M * F1) . i)
A145:
(
dom x1 c= dom x &
dom a1 c= dom a )
by RELAT_1:89;
then
x . i = (a . i) * ((M * F) . i)
by A12, A144;
then A146:
x1 . i =
(a . i) * ((M * F) . i)
by A144, FUNCT_1:70
.=
(a1 . i) * ((M * F) . i)
by A26, A31, A144, FUNCT_1:70
;
(M * F) . i =
M . (F . i)
by A11, A144, A145, FUNCT_1:23
.=
M . (F1 . i)
by A31, A144, FUNCT_1:70
.=
(M * F1) . i
by A31, A144, FUNCT_1:23
;
hence
x1 . i = (a1 . i) * ((M * F1) . i)
by A146;
:: thesis: verum
end; A147:
dom F = Seg (n + 1)
by A13, FINSEQ_1:def 3;
then A148:
dom F1 = (Seg (n + 1)) /\ (Seg n)
by RELAT_1:90;
n <= n + 1
by NAT_1:11;
then
Seg n c= Seg (n + 1)
by FINSEQ_1:7;
then A149:
dom F1 = Seg n
by A148, XBOOLE_1:28;
then A150:
len F1 = n
by FINSEQ_1:def 3;
consider G being
Finite_Sep_Sequence of
S,
b,
y being
FinSequence of
ExtREAL such that A151:
G,
b are_Re-presentation_of f | (union (rng (F | (Seg n))))
and A152:
b . 1
= 0.
and A153:
for
n being
Nat st 2
<= n &
n in dom b holds
(
0. < b . n &
b . n < +infty )
and A154:
dom y = dom G
and A155:
for
n being
Nat st
n in dom y holds
y . n = (b . n) * ((M * G) . n)
and A156:
integral X,
S,
M,
(f | (union (rng (F | (Seg n))))) = Sum y
by A20, A24, A142, MESFUNC3:def 2;
now per cases
( F . (n + 1) = {} or a . (n + 1) = 0. or ( F . (n + 1) <> {} & a . (n + 1) <> 0. ) )
;
case A157:
(
F . (n + 1) = {} or
a . (n + 1) = 0. )
;
:: thesis: integral X,S,M,f = Sum xdefpred S2[
Nat,
set ]
means ( ( $1
= 1 implies $2
= (G . 1) \/ (F . (n + 1)) ) & ( 2
<= $1 implies $2
= G . $1 ) );
A158:
for
k being
Nat st
k in Seg (len G) holds
ex
x being
Element of
S st
S2[
k,
x]
consider H being
FinSequence of
S such that A165:
(
dom H = Seg (len G) & ( for
k being
Nat st
k in Seg (len G) holds
S2[
k,
H . k] ) )
from FINSEQ_1:sch 5(A158);
A166:
union (rng G) <> {}
by A142, A151, MESFUNC3:def 1;
dom G <> {}
by A166, RELAT_1:60, RELAT_1:64, ZFMISC_1:2;
then
G <> {}
by RELAT_1:60;
then
len G <> 0
;
then
0 < len G
;
then
0 + 1
<= len G
by NAT_1:13;
then A167:
1
in Seg (len G)
by FINSEQ_1:3;
deffunc H1(
Nat)
-> Element of
ExtREAL =
(b . $1) * ((M * H) . $1);
consider z being
FinSequence of
ExtREAL such that A168:
(
len z = len y & ( for
n being
Nat st
n in dom z holds
z . n = H1(
n) ) )
from FINSEQ_2:sch 1();
A170:
dom z = dom y
by A168, FINSEQ_3:31;
for
u,
v being
set st
u <> v holds
H . u misses H . v
proof
let u,
v be
set ;
:: thesis: ( u <> v implies H . u misses H . v )
assume A172:
u <> v
;
:: thesis: H . u misses H . v
per cases
( ( u in dom H & v in dom H ) or not u in dom H or not v in dom H )
;
suppose A173:
(
u in dom H &
v in dom H )
;
:: thesis: H . u misses H . vthen reconsider u1 =
u,
v1 =
v as
Element of
NAT ;
per cases
( u = 1 or u <> 1 )
;
suppose A174:
u = 1
;
:: thesis: H . u misses H . vthen A175:
H . u = (G . 1) \/ (F . (n + 1))
by A165, A173;
1
<= v1
by A165, A173, FINSEQ_1:3;
then
1
< v1
by A172, A174, XXREAL_0:1;
then A176:
1
+ 1
<= v1
by NAT_1:13;
then A177:
H . v = G . v
by A165, A173;
A178:
G . 1
misses G . v
by A172, A174, PROB_2:def 3;
F . (n + 1) misses G . v
proof
per cases
( F . (n + 1) = {} or a . (n + 1) = 0. )
by A157;
suppose A179:
a . (n + 1) = 0.
;
:: thesis: F . (n + 1) misses G . vassume
F . (n + 1) meets G . v
;
:: thesis: contradictionthen consider w being
set such that A180:
(
w in F . (n + 1) &
w in G . v )
by XBOOLE_0:3;
1
<= n + 1
by NAT_1:11;
then
n + 1
in Seg (n + 1)
by FINSEQ_1:3;
then
n + 1
in dom F
by A13, FINSEQ_1:def 3;
then A181:
f . w = 0.
by A10, A179, A180, MESFUNC3:def 1;
A182:
(
v1 in dom G &
w in G . v1 )
by A165, A173, A180, FINSEQ_1:def 3;
then
G . v1 in rng G
by FUNCT_1:12;
then
w in union (rng G)
by A180, TARSKI:def 4;
then
w in dom (f | (union (rng (F | (Seg n)))))
by A151, MESFUNC3:def 1;
then A183:
f . w =
(f | (union (rng (F | (Seg n))))) . w
by FUNCT_1:70
.=
b . v1
by A151, A182, MESFUNC3:def 1
;
v1 in dom b
by A151, A182, MESFUNC3:def 1;
hence
contradiction
by A153, A176, A181, A183;
:: thesis: verum end;
end; hence
H . u misses H . v
by A175, A177, A178, XBOOLE_1:70;
:: thesis: verum end; suppose A184:
u <> 1
;
:: thesis: H . u misses H . v
1
<= u1
by A165, A173, FINSEQ_1:3;
then
1
< u1
by A184, XXREAL_0:1;
then A185:
1
+ 1
<= u1
by NAT_1:13;
then A186:
H . u = G . u
by A165, A173;
per cases
( v = 1 or v <> 1 )
;
suppose A187:
v = 1
;
:: thesis: H . u misses H . vthen A188:
H . v = (G . 1) \/ (F . (n + 1))
by A165, A173;
A189:
G . 1
misses G . u
by A172, A187, PROB_2:def 3;
F . (n + 1) misses G . u
proof
per cases
( F . (n + 1) = {} or a . (n + 1) = 0. )
by A157;
suppose A190:
a . (n + 1) = 0.
;
:: thesis: F . (n + 1) misses G . uassume
F . (n + 1) meets G . u
;
:: thesis: contradictionthen consider w being
set such that A191:
(
w in F . (n + 1) &
w in G . u )
by XBOOLE_0:3;
1
<= n + 1
by NAT_1:11;
then
n + 1
in Seg (n + 1)
by FINSEQ_1:3;
then
n + 1
in dom F
by A13, FINSEQ_1:def 3;
then A192:
f . w = 0.
by A10, A190, A191, MESFUNC3:def 1;
A193:
(
u1 in dom G &
w in G . u1 )
by A165, A173, A191, FINSEQ_1:def 3;
then
G . u1 in rng G
by FUNCT_1:12;
then
w in union (rng G)
by A191, TARSKI:def 4;
then
w in dom (f | (union (rng (F | (Seg n)))))
by A151, MESFUNC3:def 1;
then A194:
f . w =
(f | (union (rng (F | (Seg n))))) . w
by FUNCT_1:70
.=
b . u1
by A151, A193, MESFUNC3:def 1
;
u1 in dom b
by A151, A193, MESFUNC3:def 1;
hence
contradiction
by A153, A185, A192, A194;
:: thesis: verum end;
end; hence
H . u misses H . v
by A186, A188, A189, XBOOLE_1:70;
:: thesis: verum end; end;
end; then reconsider H =
H as
Finite_Sep_Sequence of
S by PROB_2:def 3;
A196:
dom f = union (rng H)
proof
thus
dom f c= union (rng H)
:: according to XBOOLE_0:def 10 :: thesis: union (rng H) c= dom fproof
let v be
set ;
:: according to TARSKI:def 3 :: thesis: ( not v in dom f or v in union (rng H) )
assume
v in dom f
;
:: thesis: v in union (rng H)
then
v in union (rng F)
by A10, MESFUNC3:def 1;
then consider A being
set such that A197:
(
v in A &
A in rng F )
by TARSKI:def 4;
consider u being
set such that A198:
(
u in dom F &
A = F . u )
by A197, FUNCT_1:def 5;
reconsider u =
u as
Element of
NAT by A198;
u in Seg (len F)
by A198, FINSEQ_1:def 3;
then A199:
( 1
<= u &
u <= n + 1 )
by A13, FINSEQ_1:3;
per cases
( u = n + 1 or u <> n + 1 )
;
suppose
u <> n + 1
;
:: thesis: v in union (rng H)then
u < n + 1
by A199, XXREAL_0:1;
then
u <= n
by NAT_1:13;
then A200:
u in Seg n
by A199, FINSEQ_1:3;
then A201:
F1 . u in rng F1
by A149, FUNCT_1:12;
A = F1 . u
by A149, A198, A200, FUNCT_1:70;
then
v in union (rng F1)
by A197, A201, TARSKI:def 4;
then
v in union (rng G)
by A18, A151, MESFUNC3:def 1;
then consider B being
set such that A202:
(
v in B &
B in rng G )
by TARSKI:def 4;
consider w being
set such that A203:
(
w in dom G &
B = G . w )
by A202, FUNCT_1:def 5;
reconsider w =
w as
Element of
NAT by A203;
A204:
w in Seg (len G)
by A203, FINSEQ_1:def 3;
end;
end;
let v be
set ;
:: according to TARSKI:def 3 :: thesis: ( not v in union (rng H) or v in dom f )
assume
v in union (rng H)
;
:: thesis: v in dom f
then consider A being
set such that A209:
(
v in A &
A in rng H )
by TARSKI:def 4;
consider k being
set such that A210:
(
k in dom H &
A = H . k )
by A209, FUNCT_1:def 5;
reconsider k =
k as
Element of
NAT by A210;
end; A216:
dom H =
dom G
by A165, FINSEQ_1:def 3
.=
dom b
by A151, MESFUNC3:def 1
;
for
m being
Nat st
m in dom H holds
for
x being
set st
x in H . m holds
f . x = b . m
proof
let m be
Nat;
:: thesis: ( m in dom H implies for x being set st x in H . m holds
f . x = b . m )
assume A217:
m in dom H
;
:: thesis: for x being set st x in H . m holds
f . x = b . m
let x be
set ;
:: thesis: ( x in H . m implies f . x = b . m )
assume A218:
x in H . m
;
:: thesis: f . x = b . m
per cases
( m = 1 or m <> 1 )
;
suppose A219:
m = 1
;
:: thesis: f . x = b . mthen A220:
H . m = (G . 1) \/ (F . (n + 1))
by A165, A217;
per cases
( x in G . 1 or x in F . (n + 1) )
by A218, A220, XBOOLE_0:def 3;
suppose A221:
x in G . 1
;
:: thesis: f . x = b . mA222:
m in dom G
by A165, A217, FINSEQ_1:def 3;
then A223:
(f | (union (rng (F | (Seg n))))) . x = b . m
by A151, A219, A221, MESFUNC3:def 1;
G . 1
in rng G
by A219, A222, FUNCT_1:12;
then
x in union (rng G)
by A221, TARSKI:def 4;
then
x in dom (f | (union (rng (F | (Seg n)))))
by A151, MESFUNC3:def 1;
hence
f . x = b . m
by A223, FUNCT_1:70;
:: thesis: verum end; end; suppose A225:
m <> 1
;
:: thesis: f . x = b . mA226:
m in dom G
by A165, A217, FINSEQ_1:def 3;
1
<= m
by A217, FINSEQ_3:27;
then
1
< m
by A225, XXREAL_0:1;
then
1
+ 1
<= m
by NAT_1:13;
then A227:
H . m = G . m
by A165, A217;
then A228:
(f | (union (rng (F | (Seg n))))) . x = b . m
by A151, A218, A226, MESFUNC3:def 1;
G . m in rng G
by A226, FUNCT_1:12;
then
x in union (rng G)
by A218, A227, TARSKI:def 4;
then
x in dom (f | (union (rng (F | (Seg n)))))
by A151, MESFUNC3:def 1;
hence
f . x = b . m
by A228, FUNCT_1:70;
:: thesis: verum end;
end; then A229:
H,
b are_Re-presentation_of f
by A196, A216, MESFUNC3:def 1;
A230:
dom z = dom H
by A154, A165, A170, FINSEQ_1:def 3;
A231:
for
k being
Nat st
k in dom z holds
z . k = y . k
proof
let k be
Nat;
:: thesis: ( k in dom z implies z . k = y . k )
assume A232:
k in dom z
;
:: thesis: z . k = y . k
then A233:
z . k = (b . k) * ((M * H) . k)
by A168;
A234:
y . k = (b . k) * ((M * G) . k)
by A155, A170, A232;
per cases
( k = 1 or k <> 1 )
;
suppose A236:
k <> 1
;
:: thesis: z . k = y . kA237:
k in Seg (len G)
by A154, A170, A232, FINSEQ_1:def 3;
then
1
<= k
by FINSEQ_1:3;
then
1
< k
by A236, XXREAL_0:1;
then A238:
1
+ 1
<= k
by NAT_1:13;
(M * H) . k =
M . (H . k)
by A230, A232, FUNCT_1:23
.=
M . (G . k)
by A165, A237, A238
.=
(M * G) . k
by A154, A170, A232, FUNCT_1:23
;
hence
z . k = y . k
by A155, A170, A232, A233;
:: thesis: verum end;
end;
( 1
<= n + 1 &
n + 1
<= len F )
by A13, NAT_1:11;
then A239:
n + 1
in dom F
by FINSEQ_3:27;
A240:
x . (n + 1) = 0.
A245:
( not
-infty in rng x1 & not
-infty in rng <*(x . (n + 1))*> )
proof
now assume
-infty in rng x1
;
:: thesis: contradictionthen consider l being
set such that A246:
(
l in dom x1 &
x1 . l = -infty )
by FUNCT_1:def 5;
reconsider l =
l as
Element of
NAT by A246;
A247:
x . l = -infty
by A246, FUNCT_1:70;
l in (dom x) /\ (Seg n)
by A246, RELAT_1:90;
then A248:
l in dom x
by XBOOLE_0:def 4;
then A249:
(a . l) * ((M * F) . l) = -infty
by A12, A247;
per cases
( F . l <> {} or F . l = {} )
;
suppose
F . l <> {}
;
:: thesis: contradictionthen consider v being
set such that A250:
v in F . l
by XBOOLE_0:def 1;
A251:
a . l = f . v
by A10, A11, A248, A250, MESFUNC3:def 1;
A252:
F . l in rng F
by A11, A248, FUNCT_1:12;
then
v in union (rng F)
by A250, TARSKI:def 4;
then
v in dom f
by A10, MESFUNC3:def 1;
then A253:
0. <= a . l
by A9, A251;
rng F c= S
by FINSEQ_1:def 4;
then reconsider Fl =
F . l as
Element of
S by A252;
reconsider EMPTY =
{} as
Element of
S by MEASURE1:21;
EMPTY c= F . l
by XBOOLE_1:2;
then
M . {} <= M . Fl
by MEASURE1:62;
then
0. <= M . Fl
by VALUED_0:def 19;
then
0. <= (M * F) . l
by A11, A248, FUNCT_1:23;
then
0. * ((M * F) . l) <= (a . l) * ((M * F) . l)
by A253;
hence
contradiction
by A249;
:: thesis: verum end; end;
hence
not
-infty in rng x1
;
:: thesis: not -infty in rng <*(x . (n + 1))*>
hence
not
-infty in rng <*(x . (n + 1))*>
;
:: thesis: verum
end;
len x = n + 1
by A11, A13, FINSEQ_3:31;
then x =
x | (n + 1)
by FINSEQ_1:79
.=
x | (Seg (n + 1))
by FINSEQ_1:def 15
.=
x1 ^ <*(x . (n + 1))*>
by A11, A239, FINSEQ_5:11
;
then A255:
Sum x =
(Sum x1) + (Sum <*(x . (n + 1))*>)
by A245, CONVFUN1:7
.=
(Sum x1) + 0.
by A240, CONVFUN1:5
;
integral X,
S,
M,
f =
Sum z
by A7, A8, A9, A152, A153, A168, A229, A230, MESFUNC3:def 2
.=
integral X,
S,
M,
(f | (union (rng (F | (Seg n)))))
by A156, A170, A231, FINSEQ_1:17
.=
Sum x1
by A6, A20, A24, A30, A31, A142, A143, A150
.=
Sum x
by A255, XXREAL_3:4
;
hence
integral X,
S,
M,
f = Sum x
;
:: thesis: verum end; case A256:
(
F . (n + 1) <> {} &
a . (n + 1) <> 0. )
;
:: thesis: integral X,S,M,f = Sum xA257:
f is
real-valued
by A7, MESFUNC2:def 5;
( 1
<= n + 1 &
n + 1
<= len F )
by A13, NAT_1:11;
then A258:
n + 1
in dom F
by FINSEQ_3:27;
consider v being
set such that A259:
v in F . (n + 1)
by A256, XBOOLE_0:def 1;
F . (n + 1) in rng F
by A258, FUNCT_1:12;
then
v in union (rng F)
by A259, TARSKI:def 4;
then A260:
(
v in dom f &
dom f c= X )
by A10, MESFUNC3:def 1, RELAT_1:def 18;
then reconsider v =
v as
Element of
X ;
A261:
0. <= f . v
by A9, A260;
f . v = a . (n + 1)
by A10, A258, A259, MESFUNC3:def 1;
then A262:
|.(a . (n + 1)).| < +infty
by A257, A260, MESFUNC2:def 1;
A263:
0. <= a . (n + 1)
by A10, A258, A259, A261, MESFUNC3:def 1;
A264:
(
0. < a . (n + 1) &
a . (n + 1) < +infty )
by A10, A256, A258, A259, A261, A262, EXTREAL2:58, MESFUNC3:def 1;
defpred S2[
Nat,
set ]
means ( ( $1
<= len G implies $2
= G . $1 ) & ( $1
= (len G) + 1 implies $2
= F . (n + 1) ) );
A265:
for
k being
Nat st
k in Seg ((len G) + 1) holds
ex
v being
Element of
S st
S2[
k,
v]
consider H being
FinSequence of
S such that A270:
(
dom H = Seg ((len G) + 1) & ( for
k being
Nat st
k in Seg ((len G) + 1) holds
S2[
k,
H . k] ) )
from FINSEQ_1:sch 5(A265);
A271:
Seg (len H) = Seg ((len G) + 1)
by A270, FINSEQ_1:def 3;
A272:
len H = (len G) + 1
by A270, FINSEQ_1:def 3;
defpred S3[
Nat,
set ]
means ( ( $1
<= len b implies $2
= b . $1 ) & ( $1
= (len b) + 1 implies $2
= a . (n + 1) ) );
A273:
for
k being
Nat st
k in Seg ((len b) + 1) holds
ex
v being
Element of
ExtREAL st
S3[
k,
v]
consider c being
FinSequence of
ExtREAL such that A276:
(
dom c = Seg ((len b) + 1) & ( for
k being
Nat st
k in Seg ((len b) + 1) holds
S3[
k,
c . k] ) )
from FINSEQ_1:sch 5(A273);
A277:
len c = (len b) + 1
by A276, FINSEQ_1:def 3;
1
<= (len b) + 1
by NAT_1:11;
then A278:
1
in Seg ((len b) + 1)
by FINSEQ_1:3;
A279:
dom G <> {}
A280:
dom G = dom b
by A151, MESFUNC3:def 1;
then
b <> {}
by A279, RELAT_1:60;
then
len b <> 0
;
then
len b in Seg (len b)
by FINSEQ_1:5;
then
1
<= len b
by FINSEQ_1:3;
then A281:
c . 1
= 0.
by A152, A276, A278;
A282:
Seg (len G) =
dom G
by FINSEQ_1:def 3
.=
Seg (len b)
by A280, FINSEQ_1:def 3
;
then A283:
len G = len b
by FINSEQ_1:8;
A284:
len G = len y
by A154, FINSEQ_3:31;
A285:
for
m being
Nat st 2
<= m &
m in dom c holds
(
0. < c . m &
c . m < +infty )
defpred S4[
Nat,
set ]
means ( ( $1
<= len y implies $2
= (b . $1) * ((M * H) . $1) ) & ( $1
= (len y) + 1 implies $2
= (a . (n + 1)) * ((M * F) . (n + 1)) ) );
A290:
for
k being
Nat st
k in Seg ((len y) + 1) holds
ex
v being
Element of
ExtREAL st
S4[
k,
v]
consider z being
FinSequence of
ExtREAL such that A293:
(
dom z = Seg ((len y) + 1) & ( for
k being
Nat st
k in Seg ((len y) + 1) holds
S4[
k,
z . k] ) )
from FINSEQ_1:sch 5(A290);
A294:
len z = (len y) + 1
by A293, FINSEQ_1:def 3;
then
len z in Seg ((len y) + 1)
by FINSEQ_1:6;
then A295:
z . (len z) = (a . (n + 1)) * ((M * F) . (n + 1))
by A293, A294;
A296:
len y = len G
by A154, FINSEQ_3:31;
then A297:
len z = (len G) + 1
by A293, FINSEQ_1:def 3;
then A298:
len z in Seg ((len G) + 1)
by FINSEQ_1:6;
A299:
len z in dom H
by A270, A297, FINSEQ_1:6;
A300:
(M * F) . (n + 1) =
M . (F . (n + 1))
by A147, FINSEQ_1:6, FUNCT_1:23
.=
M . (H . (len z))
by A270, A297, A298
.=
(M * H) . (len z)
by A299, FUNCT_1:23
;
A301:
for
m being
Nat st
m in dom z holds
z . m = (c . m) * ((M * H) . m)
proof
let m be
Nat;
:: thesis: ( m in dom z implies z . m = (c . m) * ((M * H) . m) )
assume A302:
m in dom z
;
:: thesis: z . m = (c . m) * ((M * H) . m)
then A303:
S3[
m,
c . m]
by A276, A283, A293, A296;
per cases
( m = (len y) + 1 or m <> (len y) + 1 )
;
suppose A304:
m <> (len y) + 1
;
:: thesis: z . m = (c . m) * ((M * H) . m)
m <= (len y) + 1
by A293, A302, FINSEQ_1:3;
then
m < (len y) + 1
by A304, XXREAL_0:1;
then A305:
m <= len b
by A283, A296, NAT_1:13;
then
c . m = b . m
by A276, A283, A293, A296, A302;
hence
z . m = (c . m) * ((M * H) . m)
by A283, A293, A296, A302, A305;
:: thesis: verum end;
end;
for
i,
j being
set st
i <> j holds
H . i misses H . j
then reconsider H =
H as
Finite_Sep_Sequence of
S by PROB_2:def 3;
F | (Seg (n + 1)) = F1 ^ <*(F . (n + 1))*>
by A147, FINSEQ_1:6, FINSEQ_5:11;
then F1 ^ <*(F . (n + 1))*> =
F | (n + 1)
by FINSEQ_1:def 15
.=
F
by A13, FINSEQ_1:79
;
then A322:
rng F =
(rng F1) \/ (rng <*(F . (n + 1))*>)
by FINSEQ_1:44
.=
(rng F1) \/ {(F . (n + 1))}
by FINSEQ_1:55
;
A323:
len H =
(len G) + 1
by A270, FINSEQ_1:def 3
.=
(len G) + (len <*(F . (n + 1))*>)
by FINSEQ_1:56
.=
len (G ^ <*(F . (n + 1))*>)
by FINSEQ_1:35
;
for
k being
Nat st 1
<= k &
k <= len H holds
H . k = (G ^ <*(F . (n + 1))*>) . k
then
H = G ^ <*(F . (n + 1))*>
by A323, FINSEQ_1:18;
then A327:
rng H =
(rng G) \/ (rng <*(F . (n + 1))*>)
by FINSEQ_1:44
.=
(rng G) \/ {(F . (n + 1))}
by FINSEQ_1:55
;
A328:
dom f =
union ((rng F1) \/ {(F . (n + 1))})
by A10, A322, MESFUNC3:def 1
.=
(dom (f | (union (rng (F | (Seg n)))))) \/ (union {(F . (n + 1))})
by A18, ZFMISC_1:96
.=
(union (rng G)) \/ (union {(F . (n + 1))})
by A151, MESFUNC3:def 1
.=
union (rng H)
by A327, ZFMISC_1:96
;
for
m being
Nat st
m in dom H holds
for
v being
set st
v in H . m holds
f . v = c . m
proof
let m be
Nat;
:: thesis: ( m in dom H implies for v being set st v in H . m holds
f . v = c . m )
assume A329:
m in dom H
;
:: thesis: for v being set st v in H . m holds
f . v = c . m
then A330:
(
S2[
m,
H . m] &
S3[
m,
c . m] )
by A270, A276, A283;
A331:
( 1
<= m &
m <= (len G) + 1 )
by A270, A329, FINSEQ_1:3;
let v be
set ;
:: thesis: ( v in H . m implies f . v = c . m )
assume A332:
v in H . m
;
:: thesis: f . v = c . m
per cases
( m = (len G) + 1 or m <> (len G) + 1 )
;
suppose
m <> (len G) + 1
;
:: thesis: f . v = c . mthen A334:
m < (len G) + 1
by A331, XXREAL_0:1;
then A335:
m <= len G
by NAT_1:13;
A336:
H . m in rng H
by A329, FUNCT_1:12;
A337:
union (rng G) = union (rng F1)
by A18, A151, MESFUNC3:def 1;
m in Seg (len G)
by A331, A335, FINSEQ_1:3;
then
m in dom G
by FINSEQ_1:def 3;
then
G . m in rng G
by FUNCT_1:12;
then
(
v in union (rng F1) &
v in dom f )
by A328, A330, A332, A334, A336, A337, NAT_1:13, TARSKI:def 4;
then
v in (dom f) /\ (union (rng F1))
by XBOOLE_0:def 4;
then A338:
v in dom (f | (union (rng (F | (Seg n)))))
by RELAT_1:90;
m in Seg (len G)
by A331, A335, FINSEQ_1:3;
then
m in dom G
by FINSEQ_1:def 3;
then
(f | (union (rng (F | (Seg n))))) . v = c . m
by A151, A283, A330, A332, A334, MESFUNC3:def 1, NAT_1:13;
hence
f . v = c . m
by A338, FUNCT_1:70;
:: thesis: verum end;
end; then A339:
H,
c are_Re-presentation_of f
by A270, A276, A283, A328, MESFUNC3:def 1;
A340:
( not
-infty in rng y & not
-infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> )
proof
now assume A341:
(
-infty in rng y or
-infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> )
;
:: thesis: contradictionper cases
( -infty in rng y or -infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> )
by A341;
suppose
-infty in rng y
;
:: thesis: contradictionthen consider k being
set such that A342:
(
k in dom y &
-infty = y . k )
by FUNCT_1:def 5;
reconsider k =
k as
Element of
NAT by A342;
A343:
y . k = (b . k) * ((M * G) . k)
by A155, A342;
k in Seg (len y)
by A342, FINSEQ_1:def 3;
then A344:
1
<= k
by FINSEQ_1:3;
per cases
( k = 1 or k <> 1 )
;
suppose
k <> 1
;
:: thesis: contradictionthen
1
< k
by A344, XXREAL_0:1;
then
( 1
+ 1
<= k &
k in dom b )
by A151, A154, A342, MESFUNC3:def 1, NAT_1:13;
then A345:
(
0. < b . k &
b . k < +infty )
by A153;
(
G . k in rng G &
rng G c= S )
by A154, A342, FINSEQ_1:def 4, FUNCT_1:12;
then reconsider Gk =
G . k as
Element of
S ;
reconsider EMPTY =
{} as
Element of
S by PROB_1:10;
M . EMPTY <= M . Gk
by MEASURE1:62, XBOOLE_1:2;
then A346:
0. <= M . Gk
by VALUED_0:def 19;
(M * G) . k = M . (G . k)
by A154, A342, FUNCT_1:23;
hence
contradiction
by A342, A343, A345, A346;
:: thesis: verum end; end; end;
hence
( not
-infty in rng y & not
-infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> )
;
:: thesis: verum
end; A350:
len (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) =
(len y) + 1
by FINSEQ_2:19
.=
len z
by A293, FINSEQ_1:def 3
;
for
k being
Nat st 1
<= k &
k <= len z holds
z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k
proof
let k be
Nat;
:: thesis: ( 1 <= k & k <= len z implies z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k )
assume A351:
( 1
<= k &
k <= len z )
;
:: thesis: z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k
per cases
( k = len z or k <> len z )
;
suppose
k <> len z
;
:: thesis: z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . kthen
k < len z
by A351, XXREAL_0:1;
then A352:
k <= len y
by A294, NAT_1:13;
then A353:
k in dom y
by A351, FINSEQ_3:27;
then A354:
(y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k =
y . k
by FINSEQ_1:def 7
.=
(b . k) * ((M * G) . k)
by A155, A353
.=
(b . k) * (M . (G . k))
by A154, A353, FUNCT_1:23
;
A355:
k in Seg (len z)
by A351, FINSEQ_1:3;
then A356:
H . k = G . k
by A270, A284, A294, A352;
M . (H . k) = (M * H) . k
by A270, A284, A294, A355, FUNCT_1:23;
hence
z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k
by A293, A294, A352, A354, A355, A356;
:: thesis: verum end;
end; then A357:
z = y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>
by A350, FINSEQ_1:18;
A358:
not
-infty in rng x1
proof
assume
-infty in rng x1
;
:: thesis: contradiction
then consider k being
set such that A359:
(
k in dom x1 &
-infty = x1 . k )
by FUNCT_1:def 5;
reconsider k =
k as
Element of
NAT by A359;
A360:
x . k = -infty
by A359, FUNCT_1:70;
k in (dom x) /\ (Seg n)
by A359, RELAT_1:90;
then A361:
k in dom x
by XBOOLE_0:def 4;
then A362:
x . k = (a . k) * ((M * F) . k)
by A12;
reconsider EMPTY =
{} as
Element of
S by PROB_1:10;
A363:
F . k in rng F
by A11, A361, FUNCT_1:12;
rng F c= S
by FINSEQ_1:def 4;
then reconsider Fk =
F . k as
Element of
S by A363;
per cases
( F . k <> {} or F . k = {} )
;
suppose
F . k <> {}
;
:: thesis: contradictionthen consider v being
set such that A364:
v in F . k
by XBOOLE_0:def 1;
A365:
a . k = f . v
by A10, A11, A361, A364, MESFUNC3:def 1;
v in union (rng F)
by A363, A364, TARSKI:def 4;
then
v in dom f
by A10, MESFUNC3:def 1;
then A366:
0. <= a . k
by A9, A365;
M . EMPTY <= M . Fk
by MEASURE1:62, XBOOLE_1:2;
then A367:
0. <= M . Fk
by VALUED_0:def 19;
M . Fk = (M * F) . k
by A11, A361, FUNCT_1:23;
hence
contradiction
by A360, A362, A366, A367;
:: thesis: verum end;
end;
len x = n + 1
by A11, A13, FINSEQ_3:31;
then A368:
x =
x | (n + 1)
by FINSEQ_1:79
.=
x | (Seg (n + 1))
by FINSEQ_1:def 15
.=
x1 ^ <*(x . (n + 1))*>
by A11, A258, FINSEQ_5:11
.=
x1 ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>
by A11, A12, A258
;
integral X,
S,
M,
f =
Sum z
by A7, A8, A9, A270, A281, A285, A293, A296, A301, A339, MESFUNC3:def 2
.=
(Sum y) + (Sum <*((a . (n + 1)) * ((M * H) . (len z)))*>)
by A300, A340, A357, CONVFUN1:7
.=
(integral X,S,M,(f | (union (rng (F | (Seg n)))))) + ((a . (n + 1)) * ((M * H) . (len z)))
by A156, CONVFUN1:5
.=
(Sum x1) + ((a . (n + 1)) * ((M * F) . (n + 1)))
by A6, A20, A24, A30, A31, A142, A143, A150, A300
.=
(Sum x1) + (Sum <*((a . (n + 1)) * ((M * F) . (n + 1)))*>)
by CONVFUN1:5
.=
Sum x
by A340, A358, A368, CONVFUN1:7
;
hence
integral X,
S,
M,
f = Sum x
;
:: thesis: verum end; hence
integral X,
S,
M,
f = Sum x
;
:: thesis: verum end;
hence
integral X,
S,
M,
f = Sum x
;
:: thesis: verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A5);
hence
for n being Nat
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) & len F = n holds
integral X,S,M,f = Sum x
; :: thesis: verum