let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative & ( for x being set st x in dom f holds
g . x <= f . x ) holds
( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative & ( for x being set st x in dom f holds
g . x <= f . x ) holds
( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )
let M be sigma_Measure of S; for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative & ( for x being set st x in dom f holds
g . x <= f . x ) holds
( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )
let f, g be PartFunc of X,ExtREAL; ( f is_simple_func_in S & dom f <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative & ( for x being set st x in dom f holds
g . x <= f . x ) implies ( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) ) )
assume that
A1:
f is_simple_func_in S
and
A2:
dom f <> {}
and
A3:
f is nonnegative
and
A4:
g is_simple_func_in S
and
A5:
dom g = dom f
and
A6:
g is nonnegative
and
A7:
for x being set st x in dom f holds
g . x <= f . x
; ( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )
consider G being Finite_Sep_Sequence of S, b, y being FinSequence of ExtREAL such that
A9:
G,b are_Re-presentation_of g
and
dom y = dom G
and
for n being Nat st n in dom y holds
y . n = (b . n) * ((M * G) . n)
and
integral (M,g) = Sum y
by A2, A4, A5, A6, MESFUNC4:4;
g is real-valued
by A4, MESFUNC2:def 4;
then A10:
dom (f - g) = (dom f) /\ (dom g)
by MESFUNC2:2;
consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A12:
F,a are_Re-presentation_of f
and
dom x = dom F
and
for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n)
and
integral (M,f) = Sum x
by A1, A2, MESFUNC4:4, A3;
set la = len a;
A13:
dom F = dom a
by A12, MESFUNC3:def 1;
set lb = len b;
deffunc H1( Nat) -> set = (F . ((($1 -' 1) div (len b)) + 1)) /\ (G . ((($1 -' 1) mod (len b)) + 1));
consider FG being FinSequence such that
A14:
len FG = (len a) * (len b)
and
A15:
for k being Nat st k in dom FG holds
FG . k = H1(k)
from FINSEQ_1:sch 2();
A16:
dom FG = Seg ((len a) * (len b))
by A14, FINSEQ_1:def 3;
A17:
dom G = dom b
by A9, MESFUNC3:def 1;
FG is FinSequence of S
proof
let b be
object ;
TARSKI:def 3,
FINSEQ_1:def 4 ( not b in rng FG or b in S )
A18:
now for k being Element of NAT st k in dom FG holds
FG . k in Slet k be
Element of
NAT ;
( k in dom FG implies FG . k in S )set i =
((k -' 1) div (len b)) + 1;
set j =
((k -' 1) mod (len b)) + 1;
A19:
len b divides (len a) * (len b)
by NAT_D:def 3;
assume A20:
k in dom FG
;
FG . k in Sthen A21:
k in Seg ((len a) * (len b))
by A14, FINSEQ_1:def 3;
then A22:
k <= (len a) * (len b)
by FINSEQ_1:1;
then
k -' 1
<= ((len a) * (len b)) -' 1
by NAT_D:42;
then A23:
(k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b)
by NAT_2:24;
1
<= k
by A21, FINSEQ_1:1;
then A24:
1
<= (len a) * (len b)
by A22, XXREAL_0:2;
A25:
len b <> 0
by A21;
then
(k -' 1) mod (len b) < len b
by NAT_D:1;
then A26:
((k -' 1) mod (len b)) + 1
<= len b
by NAT_1:13;
len b >= 0 + 1
by A25, NAT_1:13;
then
(((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1
by A19, A24, NAT_2:15;
then
((k -' 1) div (len b)) + 1
<= ((len a) * (len b)) div (len b)
by A23, XREAL_1:19;
then A27:
((k -' 1) div (len b)) + 1
<= len a
by A25, NAT_D:18;
((k -' 1) div (len b)) + 1
>= 0 + 1
by XREAL_1:6;
then
((k -' 1) div (len b)) + 1
in Seg (len a)
by A27;
then
((k -' 1) div (len b)) + 1
in dom F
by A13, FINSEQ_1:def 3;
then A28:
F . (((k -' 1) div (len b)) + 1) in rng F
by FUNCT_1:3;
((k -' 1) mod (len b)) + 1
>= 0 + 1
by XREAL_1:6;
then
((k -' 1) mod (len b)) + 1
in Seg (len b)
by A26;
then
((k -' 1) mod (len b)) + 1
in dom G
by A17, FINSEQ_1:def 3;
then A29:
G . (((k -' 1) mod (len b)) + 1) in rng G
by FUNCT_1:3;
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))
by A15, A20;
hence
FG . k in S
by A28, A29, MEASURE1:34;
verum end;
assume
b in rng FG
;
b in S
then
ex
a being
object st
(
a in dom FG &
b = FG . a )
by FUNCT_1:def 3;
hence
b in S
by A18;
verum
end;
then reconsider FG = FG as FinSequence of S ;
for k, l being Nat st k in dom FG & l in dom FG & k <> l holds
FG . k misses FG . l
proof
let k,
l be
Nat;
( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )
assume that A30:
k in dom FG
and A31:
l in dom FG
and A32:
k <> l
;
FG . k misses FG . l
A33:
k in Seg ((len a) * (len b))
by A14, A30, FINSEQ_1:def 3;
then A34:
1
<= k
by FINSEQ_1:1;
set m =
((l -' 1) mod (len b)) + 1;
set n =
((l -' 1) div (len b)) + 1;
set j =
((k -' 1) mod (len b)) + 1;
set i =
((k -' 1) div (len b)) + 1;
A35:
len b divides (len a) * (len b)
by NAT_D:def 3;
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))
by A15, A30;
then A36:
(FG . k) /\ (FG . l) =
((F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))
by A15, A31
.=
(F . (((k -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))))
by XBOOLE_1:16
.=
(F . (((k -' 1) div (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))))
by XBOOLE_1:16
.=
((F . (((k -' 1) div (len b)) + 1)) /\ (F . (((l -' 1) div (len b)) + 1))) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))
by XBOOLE_1:16
;
A37:
k <= (len a) * (len b)
by A33, FINSEQ_1:1;
then A38:
1
<= (len a) * (len b)
by A34, XXREAL_0:2;
A39:
len b <> 0
by A33;
then
len b >= 0 + 1
by NAT_1:13;
then A40:
(((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1
by A35, A38, NAT_2:15;
k -' 1
<= ((len a) * (len b)) -' 1
by A37, NAT_D:42;
then
(k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1
by A40, NAT_2:24;
then
((k -' 1) div (len b)) + 1
<= ((len a) * (len b)) div (len b)
by XREAL_1:19;
then A41:
((k -' 1) div (len b)) + 1
<= len a
by A39, NAT_D:18;
((k -' 1) div (len b)) + 1
>= 0 + 1
by XREAL_1:6;
then
((k -' 1) div (len b)) + 1
in Seg (len a)
by A41;
then A42:
((k -' 1) div (len b)) + 1
in dom F
by A13, FINSEQ_1:def 3;
(l -' 1) mod (len b) < len b
by A39, NAT_D:1;
then A43:
((l -' 1) mod (len b)) + 1
<= len b
by NAT_1:13;
((l -' 1) mod (len b)) + 1
>= 0 + 1
by XREAL_1:6;
then
((l -' 1) mod (len b)) + 1
in Seg (len b)
by A43;
then A44:
((l -' 1) mod (len b)) + 1
in dom G
by A17, FINSEQ_1:def 3;
(k -' 1) mod (len b) < len b
by A39, NAT_D:1;
then A45:
((k -' 1) mod (len b)) + 1
<= len b
by NAT_1:13;
((k -' 1) mod (len b)) + 1
>= 0 + 1
by XREAL_1:6;
then
((k -' 1) mod (len b)) + 1
in Seg (len b)
by A45;
then A46:
((k -' 1) mod (len b)) + 1
in dom G
by A17, FINSEQ_1:def 3;
A47:
l in Seg ((len a) * (len b))
by A14, A31, FINSEQ_1:def 3;
then A48:
1
<= l
by FINSEQ_1:1;
l <= (len a) * (len b)
by A47, FINSEQ_1:1;
then
l -' 1
<= ((len a) * (len b)) -' 1
by NAT_D:42;
then
(l -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1
by A40, NAT_2:24;
then
((l -' 1) div (len b)) + 1
<= ((len a) * (len b)) div (len b)
by XREAL_1:19;
then A53:
((l -' 1) div (len b)) + 1
<= len a
by A39, NAT_D:18;
((l -' 1) div (len b)) + 1
>= 0 + 1
by XREAL_1:6;
then
((l -' 1) div (len b)) + 1
in Seg (len a)
by A53;
then A54:
((l -' 1) div (len b)) + 1
in dom F
by A13, FINSEQ_1:def 3;
end;
then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A55:
dom f = union (rng F)
by A12, MESFUNC3:def 1;
defpred S1[ Nat, set ] means ( ( G . ((($1 -' 1) mod (len b)) + 1) = {} implies $2 = 0 ) & ( G . ((($1 -' 1) mod (len b)) + 1) <> {} implies $2 = b . ((($1 -' 1) mod (len b)) + 1) ) );
defpred S2[ Nat, set ] means ( ( F . ((($1 -' 1) div (len b)) + 1) = {} implies $2 = 0 ) & ( F . ((($1 -' 1) div (len b)) + 1) <> {} implies $2 = a . ((($1 -' 1) div (len b)) + 1) ) );
A56:
for k being Nat st k in Seg (len FG) holds
ex v being Element of ExtREAL st S2[k,v]
consider a1 being FinSequence of ExtREAL such that
A59:
( dom a1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds
S2[k,a1 . k] ) )
from FINSEQ_1:sch 5(A56);
A60:
dom g = union (rng G)
by A9, MESFUNC3:def 1;
A61:
dom f = union (rng FG)
proof
thus
dom f c= union (rng FG)
XBOOLE_0:def 10 union (rng FG) c= dom fproof
let z be
object ;
TARSKI:def 3 ( not z in dom f or z in union (rng FG) )
assume A62:
z in dom f
;
z in union (rng FG)
then consider Y being
set such that A63:
z in Y
and A64:
Y in rng F
by A55, TARSKI:def 4;
consider i being
Nat such that A65:
i in dom F
and A66:
Y = F . i
by A64, FINSEQ_2:10;
A67:
i in Seg (len a)
by A13, A65, FINSEQ_1:def 3;
then
1
<= i
by FINSEQ_1:1;
then consider i9 being
Nat such that A68:
i = 1
+ i9
by NAT_1:10;
consider Z being
set such that A69:
z in Z
and A70:
Z in rng G
by A5, A60, A62, TARSKI:def 4;
consider j being
Nat such that A71:
j in dom G
and A72:
Z = G . j
by A70, FINSEQ_2:10;
A73:
j in Seg (len b)
by A17, A71, FINSEQ_1:def 3;
then A74:
1
<= j
by FINSEQ_1:1;
then consider j9 being
Nat such that A75:
j = 1
+ j9
by NAT_1:10;
(i9 * (len b)) + j in NAT
by ORDINAL1:def 12;
then reconsider k =
((i - 1) * (len b)) + j as
Element of
NAT by A68;
i <= len a
by A67, FINSEQ_1:1;
then
i - 1
<= (len a) - 1
by XREAL_1:9;
then
(i - 1) * (len b) <= ((len a) - 1) * (len b)
by XREAL_1:64;
then A76:
k <= (((len a) - 1) * (len b)) + j
by XREAL_1:6;
A77:
k >= 0 + j
by A68, XREAL_1:6;
then
k -' 1
= k - 1
by A74, XREAL_1:233, XXREAL_0:2;
then A78:
k -' 1
= (i9 * (len b)) + j9
by A68, A75;
A79:
j <= len b
by A73, FINSEQ_1:1;
then
(((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b)
by XREAL_1:6;
then A80:
k <= (len a) * (len b)
by A76, XXREAL_0:2;
k >= 1
by A74, A77, XXREAL_0:2;
then A81:
k in Seg ((len a) * (len b))
by A80;
then
k in dom FG
by A14, FINSEQ_1:def 3;
then A82:
FG . k in rng FG
by FUNCT_1:def 3;
A83:
j9 < len b
by A79, A75, NAT_1:13;
then A84:
j = ((k -' 1) mod (len b)) + 1
by A75, A78, NAT_D:def 2;
A85:
i = ((k -' 1) div (len b)) + 1
by A68, A78, A83, NAT_D:def 1;
z in (F . i) /\ (G . j)
by A63, A66, A69, A72, XBOOLE_0:def 4;
then
z in FG . k
by A15, A16, A85, A84, A81;
hence
z in union (rng FG)
by A82, TARSKI:def 4;
verum
end;
let z be
object ;
TARSKI:def 3 ( not z in union (rng FG) or z in dom f )
A86:
len b divides (len a) * (len b)
by NAT_D:def 3;
assume
z in union (rng FG)
;
z in dom f
then consider Y being
set such that A87:
z in Y
and A88:
Y in rng FG
by TARSKI:def 4;
consider k being
Nat such that A89:
k in dom FG
and A90:
Y = FG . k
by A88, FINSEQ_2:10;
set i =
((k -' 1) div (len b)) + 1;
A91:
k in Seg (len FG)
by A89, FINSEQ_1:def 3;
then A92:
k <= (len a) * (len b)
by A14, FINSEQ_1:1;
then A93:
k -' 1
<= ((len a) * (len b)) -' 1
by NAT_D:42;
1
<= k
by A91, FINSEQ_1:1;
then A94:
1
<= (len a) * (len b)
by A92, XXREAL_0:2;
A95:
len b <> 0
by A14, A91;
then
len b >= 0 + 1
by NAT_1:13;
then
(((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1
by A86, A94, NAT_2:15;
then
(k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1
by A93, NAT_2:24;
then A96:
((k -' 1) div (len b)) + 1
<= ((len a) * (len b)) div (len b)
by XREAL_1:19;
set j =
((k -' 1) mod (len b)) + 1;
A97:
((k -' 1) div (len b)) + 1
>= 0 + 1
by XREAL_1:6;
((len a) * (len b)) div (len b) = len a
by A95, NAT_D:18;
then
((k -' 1) div (len b)) + 1
in Seg (len a)
by A97, A96;
then
((k -' 1) div (len b)) + 1
in dom F
by A13, FINSEQ_1:def 3;
then A98:
F . (((k -' 1) div (len b)) + 1) in rng F
by FUNCT_1:def 3;
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))
by A15, A89;
then
z in F . (((k -' 1) div (len b)) + 1)
by A87, A90, XBOOLE_0:def 4;
hence
z in dom f
by A55, A98, TARSKI:def 4;
verum
end;
A99:
for k being Nat
for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
(f - g) . x = (f - g) . y
proof
let k be
Nat;
for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
(f - g) . x = (f - g) . ylet x,
y be
Element of
X;
( k in dom FG & x in FG . k & y in FG . k implies (f - g) . x = (f - g) . y )
assume that A100:
k in dom FG
and A101:
x in FG . k
and A102:
y in FG . k
;
(f - g) . x = (f - g) . y
set j =
((k -' 1) mod (len b)) + 1;
A103:
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))
by A15, A100;
then A104:
x in G . (((k -' 1) mod (len b)) + 1)
by A101, XBOOLE_0:def 4;
set i =
((k -' 1) div (len b)) + 1;
A105:
((k -' 1) div (len b)) + 1
>= 0 + 1
by XREAL_1:6;
A106:
k in Seg (len FG)
by A100, FINSEQ_1:def 3;
then A107:
1
<= k
by FINSEQ_1:1;
A108:
len b > 0
by A14, A106;
then A109:
len b >= 0 + 1
by NAT_1:13;
A110:
y in G . (((k -' 1) mod (len b)) + 1)
by A102, A103, XBOOLE_0:def 4;
A111:
len b divides (len a) * (len b)
by NAT_D:def 3;
A112:
k <= (len a) * (len b)
by A14, A106, FINSEQ_1:1;
then A113:
k -' 1
<= ((len a) * (len b)) -' 1
by NAT_D:42;
1
<= (len a) * (len b)
by A107, A112, XXREAL_0:2;
then
(((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1
by A109, A111, NAT_2:15;
then
(k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1
by A113, NAT_2:24;
then A114:
((k -' 1) div (len b)) + 1
<= ((len a) * (len b)) div (len b)
by XREAL_1:19;
len b <> 0
by A14, A106;
then
((k -' 1) div (len b)) + 1
<= len a
by A114, NAT_D:18;
then
((k -' 1) div (len b)) + 1
in Seg (len a)
by A105;
then A115:
((k -' 1) div (len b)) + 1
in dom F
by A13, FINSEQ_1:def 3;
(k -' 1) mod (len b) < len b
by A108, NAT_D:1;
then A116:
((k -' 1) mod (len b)) + 1
<= len b
by NAT_1:13;
((k -' 1) mod (len b)) + 1
>= 0 + 1
by XREAL_1:6;
then
((k -' 1) mod (len b)) + 1
in Seg (len b)
by A116;
then A117:
((k -' 1) mod (len b)) + 1
in dom G
by A17, FINSEQ_1:def 3;
y in F . (((k -' 1) div (len b)) + 1)
by A102, A103, XBOOLE_0:def 4;
then A118:
f . y = a . (((k -' 1) div (len b)) + 1)
by A12, A115, MESFUNC3:def 1;
x in F . (((k -' 1) div (len b)) + 1)
by A101, A103, XBOOLE_0:def 4;
then A119:
f . x = a . (((k -' 1) div (len b)) + 1)
by A12, A115, MESFUNC3:def 1;
A120:
FG . k in rng FG
by A100, FUNCT_1:def 3;
then A121:
y in dom (f - g)
by A5, A61, A10, A102, TARSKI:def 4;
x in dom (f - g)
by A5, A61, A10, A101, A120, TARSKI:def 4;
then (f - g) . x =
(f . x) - (g . x)
by MESFUNC1:def 4
.=
(a . (((k -' 1) div (len b)) + 1)) - (b . (((k -' 1) mod (len b)) + 1))
by A9, A117, A104, A119, MESFUNC3:def 1
.=
(f . y) - (g . y)
by A9, A117, A110, A118, MESFUNC3:def 1
;
hence
(f - g) . x = (f - g) . y
by A121, MESFUNC1:def 4;
verum
end;
deffunc H2( Nat) -> Element of ExtREAL = (a1 . $1) * ((M * FG) . $1);
consider x1 being FinSequence of ExtREAL such that
A122:
( len x1 = len FG & ( for k being Nat st k in dom x1 holds
x1 . k = H2(k) ) )
from FINSEQ_2:sch 1();
A123:
for k being Nat st k in dom FG holds
for x being object st x in FG . k holds
f . x = a1 . k
proof
let k be
Nat;
( k in dom FG implies for x being object st x in FG . k holds
f . x = a1 . k )
set i =
((k -' 1) div (len b)) + 1;
A124:
((k -' 1) div (len b)) + 1
>= 0 + 1
by XREAL_1:6;
assume A125:
k in dom FG
;
for x being object st x in FG . k holds
f . x = a1 . k
then A126:
k in Seg (len FG)
by FINSEQ_1:def 3;
let x be
object ;
( x in FG . k implies f . x = a1 . k )
assume A127:
x in FG . k
;
f . x = a1 . k
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))
by A15, A125;
then A128:
x in F . (((k -' 1) div (len b)) + 1)
by A127, XBOOLE_0:def 4;
A129:
k in Seg (len FG)
by A125, FINSEQ_1:def 3;
then A130:
k <= (len a) * (len b)
by A14, FINSEQ_1:1;
then
k -' 1
<= ((len a) * (len b)) -' 1
by NAT_D:42;
then A131:
(k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b)
by NAT_2:24;
A132:
len b divides (len a) * (len b)
by NAT_D:def 3;
1
<= k
by A129, FINSEQ_1:1;
then A133:
1
<= (len a) * (len b)
by A130, XXREAL_0:2;
A134:
len b <> 0
by A14, A129;
then
len b >= 0 + 1
by NAT_1:13;
then
(((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1
by A132, A133, NAT_2:15;
then A135:
((k -' 1) div (len b)) + 1
<= ((len a) * (len b)) div (len b)
by A131, XREAL_1:19;
((len a) * (len b)) div (len b) = len a
by A134, NAT_D:18;
then
((k -' 1) div (len b)) + 1
in Seg (len a)
by A124, A135;
then
((k -' 1) div (len b)) + 1
in dom F
by A13, FINSEQ_1:def 3;
then
f . x = a . (((k -' 1) div (len b)) + 1)
by A12, A128, MESFUNC3:def 1;
hence
f . x = a1 . k
by A59, A126, A128;
verum
end;
A136:
for k being Nat st k in Seg (len FG) holds
ex v being Element of ExtREAL st S1[k,v]
consider b1 being FinSequence of ExtREAL such that
A139:
( dom b1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds
S1[k,b1 . k] ) )
from FINSEQ_1:sch 5(A136);
deffunc H3( Nat) -> Element of ExtREAL = (a1 . $1) - (b1 . $1);
consider c1 being FinSequence of ExtREAL such that
A140:
len c1 = len FG
and
A141:
for k being Nat st k in dom c1 holds
c1 . k = H3(k)
from FINSEQ_2:sch 1();
A142:
dom c1 = Seg (len FG)
by A140, FINSEQ_1:def 3;
A143:
for k being Nat st k in dom FG holds
for x being object st x in FG . k holds
g . x = b1 . k
A149:
for k being Nat st k in dom FG holds
for x being object st x in FG . k holds
(f - g) . x = c1 . k
proof
let k be
Nat;
( k in dom FG implies for x being object st x in FG . k holds
(f - g) . x = c1 . k )
assume A150:
k in dom FG
;
for x being object st x in FG . k holds
(f - g) . x = c1 . k
let x be
object ;
( x in FG . k implies (f - g) . x = c1 . k )
assume A151:
x in FG . k
;
(f - g) . x = c1 . k
FG . k in rng FG
by A150, FUNCT_1:def 3;
then
x in dom (f - g)
by A5, A61, A10, A151, TARSKI:def 4;
then A152:
(f - g) . x = (f . x) - (g . x)
by MESFUNC1:def 4;
k in Seg (len FG)
by A150, FINSEQ_1:def 3;
then
(a1 . k) - (b1 . k) = c1 . k
by A141, A142;
then
(a1 . k) - (g . x) = c1 . k
by A143, A150, A151;
hence
(f - g) . x = c1 . k
by A123, A150, A151, A152;
verum
end;
deffunc H4( Nat) -> Element of ExtREAL = (c1 . $1) * ((M * FG) . $1);
consider z1 being FinSequence of ExtREAL such that
A153:
( len z1 = len FG & ( for k being Nat st k in dom z1 holds
z1 . k = H4(k) ) )
from FINSEQ_2:sch 1();
deffunc H5( Nat) -> Element of ExtREAL = (b1 . $1) * ((M * FG) . $1);
consider y1 being FinSequence of ExtREAL such that
A154:
( len y1 = len FG & ( for k being Nat st k in dom y1 holds
y1 . k = H5(k) ) )
from FINSEQ_2:sch 1();
A155:
dom x1 = dom FG
by A122, FINSEQ_3:29;
A156:
dom z1 = dom FG
by A153, FINSEQ_3:29;
A157:
for i being Nat st i in dom x1 holds
0 <= z1 . i
proof
reconsider EMPTY =
{} as
Element of
S by PROB_1:4;
let i be
Nat;
( i in dom x1 implies 0 <= z1 . i )
assume A158:
i in dom x1
;
0 <= z1 . i
then A159:
(M * FG) . i = M . (FG . i)
by A155, FUNCT_1:13;
FG . i in rng FG
by A155, A158, FUNCT_1:3;
then reconsider V =
FG . i as
Element of
S ;
M . EMPTY <= M . V
by MEASURE1:31, XBOOLE_1:2;
then A160:
0 <= (M * FG) . i
by A159, VALUED_0:def 19;
A161:
i in Seg (len FG)
by A122, A158, FINSEQ_1:def 3;
per cases
( FG . i <> {} or FG . i = {} )
;
suppose
FG . i <> {}
;
0 <= z1 . ithen consider x being
object such that A162:
x in FG . i
by XBOOLE_0:def 1;
FG . i in rng FG
by A155, A158, FUNCT_1:3;
then
x in union (rng FG)
by A162, TARSKI:def 4;
then
g . x <= f . x
by A7, A61;
then
g . x <= a1 . i
by A155, A123, A158, A162;
then
b1 . i <= a1 . i
by A155, A143, A158, A162;
then
0 <= (a1 . i) - (b1 . i)
by XXREAL_3:40;
then
0 <= c1 . i
by A141, A142, A161;
then
0 <= (c1 . i) * ((M * FG) . i)
by A160;
hence
0 <= z1 . i
by A155, A153, A156, A158;
verum end;
end;
then
for i being object st i in dom z1 holds
0 <= z1 . i
by A156, A155;
then cd:
z1 is nonnegative
by SUPINF_2:52;
not -infty in rng z1
then A163: (z1 " {-infty}) /\ (y1 " {+infty}) =
{} /\ (y1 " {+infty})
by FUNCT_1:72
.=
{}
;
A164:
dom y1 = dom FG
by A154, FINSEQ_3:29;
A165:
for i being Nat st i in dom y1 holds
0 <= y1 . i
proof
let i be
Nat;
( i in dom y1 implies 0 <= y1 . i )
set i9 =
((i -' 1) mod (len b)) + 1;
A166:
((i -' 1) mod (len b)) + 1
>= 0 + 1
by XREAL_1:6;
assume A167:
i in dom y1
;
0 <= y1 . i
then A168:
y1 . i = (b1 . i) * ((M * FG) . i)
by A154;
A169:
i in Seg (len FG)
by A154, A167, FINSEQ_1:def 3;
then
len b <> 0
by A14;
then
(i -' 1) mod (len b) < len b
by NAT_D:1;
then
((i -' 1) mod (len b)) + 1
<= len b
by NAT_1:13;
then
((i -' 1) mod (len b)) + 1
in Seg (len b)
by A166;
then A170:
((i -' 1) mod (len b)) + 1
in dom G
by A17, FINSEQ_1:def 3;
per cases
( G . (((i -' 1) mod (len b)) + 1) <> {} or G . (((i -' 1) mod (len b)) + 1) = {} )
;
suppose A171:
G . (((i -' 1) mod (len b)) + 1) <> {}
;
0 <= y1 . i
FG . i in rng FG
by A164, A167, FUNCT_1:3;
then reconsider FGi =
FG . i as
Element of
S ;
reconsider EMPTY =
{} as
Element of
S by MEASURE1:7;
EMPTY c= FGi
;
then A172:
M . {} <= M . FGi
by MEASURE1:31;
consider x9 being
object such that A173:
x9 in G . (((i -' 1) mod (len b)) + 1)
by A171, XBOOLE_0:def 1;
g . x9 =
b . (((i -' 1) mod (len b)) + 1)
by A9, A170, A173, MESFUNC3:def 1
.=
b1 . i
by A139, A169, A171
;
then A174:
0 <= b1 . i
by A6, SUPINF_2:51;
M . {} = 0
by VALUED_0:def 19;
then
0 <= (M * FG) . i
by A164, A167, A172, FUNCT_1:13;
hence
0 <= y1 . i
by A168, A174;
verum end;
end;
then
for i being object st i in dom y1 holds
0 <= y1 . i
;
then ag:
y1 is nonnegative
by SUPINF_2:52;
not -infty in rng y1
then (z1 " {+infty}) /\ (y1 " {-infty}) =
(z1 " {+infty}) /\ {}
by FUNCT_1:72
.=
{}
;
then A176: dom (z1 + y1) =
((dom z1) /\ (dom y1)) \ ({} \/ {})
by A163, MESFUNC1:def 3
.=
dom x1
by A122, A164, A156, FINSEQ_3:29
;
A177:
for k being Nat st k in dom x1 holds
x1 . k = (z1 + y1) . k
proof
A178:
len b divides (len a) * (len b)
by NAT_D:def 3;
let k be
Nat;
( k in dom x1 implies x1 . k = (z1 + y1) . k )
set p =
((k -' 1) div (len b)) + 1;
set q =
((k -' 1) mod (len b)) + 1;
A179:
((k -' 1) div (len b)) + 1
>= 0 + 1
by XREAL_1:6;
assume A180:
k in dom x1
;
x1 . k = (z1 + y1) . k
then A181:
k in Seg (len FG)
by A122, FINSEQ_1:def 3;
then A182:
1
<= k
by FINSEQ_1:1;
A183:
len b > 0
by A14, A181;
then A184:
len b >= 0 + 1
by NAT_1:13;
A185:
k <= (len a) * (len b)
by A14, A181, FINSEQ_1:1;
then A186:
k -' 1
<= ((len a) * (len b)) -' 1
by NAT_D:42;
1
<= (len a) * (len b)
by A182, A185, XXREAL_0:2;
then
(((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1
by A184, A178, NAT_2:15;
then
(k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1
by A186, NAT_2:24;
then A187:
((k -' 1) div (len b)) + 1
<= ((len a) * (len b)) div (len b)
by XREAL_1:19;
len b <> 0
by A14, A181;
then
((k -' 1) div (len b)) + 1
<= len a
by A187, NAT_D:18;
then
((k -' 1) div (len b)) + 1
in Seg (len a)
by A179;
then A188:
((k -' 1) div (len b)) + 1
in dom F
by A13, FINSEQ_1:def 3;
A189:
((k -' 1) mod (len b)) + 1
>= 0 + 1
by XREAL_1:6;
(k -' 1) mod (len b) < len b
by A183, NAT_D:1;
then
((k -' 1) mod (len b)) + 1
<= len b
by NAT_1:13;
then
((k -' 1) mod (len b)) + 1
in Seg (len b)
by A189;
then A190:
((k -' 1) mod (len b)) + 1
in dom G
by A17, FINSEQ_1:def 3;
A191:
((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))
proof
per cases
( FG . k <> {} or FG . k = {} )
;
suppose
FG . k <> {}
;
((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))then
(F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) <> {}
by A14, A15, A16, A181;
then consider v being
object such that A192:
v in (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))
by XBOOLE_0:def 1;
A193:
G . (((k -' 1) mod (len b)) + 1) <> {}
by A192;
A194:
v in F . (((k -' 1) div (len b)) + 1)
by A192, XBOOLE_0:def 4;
v in G . (((k -' 1) mod (len b)) + 1)
by A192, XBOOLE_0:def 4;
then A195:
b . (((k -' 1) mod (len b)) + 1) = g . v
by A9, A190, MESFUNC3:def 1;
F . (((k -' 1) div (len b)) + 1) in rng F
by A188, FUNCT_1:3;
then A196:
v in dom f
by A55, A194, TARSKI:def 4;
a . (((k -' 1) div (len b)) + 1) = f . v
by A12, A188, A194, MESFUNC3:def 1;
then
b . (((k -' 1) mod (len b)) + 1) <= a . (((k -' 1) div (len b)) + 1)
by A7, A195, A196;
then A197:
b1 . k <= a . (((k -' 1) div (len b)) + 1)
by A139, A181, A193;
F . (((k -' 1) div (len b)) + 1) <> {}
by A192;
then
b1 . k <= a1 . k
by A59, A181, A197;
then
0 <= (a1 . k) - (b1 . k)
by XXREAL_3:40;
then A198:
(
0 = c1 . k or
0 < c1 . k )
by A141, A142, A181;
0 <= b . (((k -' 1) mod (len b)) + 1)
by A6, A195, SUPINF_2:51;
then
(
0 = b1 . k or
0 < b1 . k )
by A139, A181, A192;
hence
((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))
by A198, XXREAL_3:96;
verum end;
end;
A200:
(
a1 . k <> +infty &
a1 . k <> -infty &
b1 . k <> +infty &
b1 . k <> -infty )
A207:
(b1 . k) - (b1 . k) = - 0
by XXREAL_3:7;
c1 . k = (a1 . k) - (b1 . k)
by A141, A142, A181;
then (c1 . k) + (b1 . k) =
(a1 . k) - ((b1 . k) - (b1 . k))
by A200, XXREAL_3:32
.=
(a1 . k) + (- 0)
by A207
.=
a1 . k
by XXREAL_3:4
;
hence x1 . k =
((c1 . k) + (b1 . k)) * ((M * FG) . k)
by A122, A180
.=
(z1 . k) + ((b1 . k) * ((M * FG) . k))
by A155, A153, A156, A180, A191
.=
(z1 . k) + (y1 . k)
by A155, A154, A164, A180
.=
(z1 + y1) . k
by A176, A180, MESFUNC1:def 3
;
verum
end;
now for x being Element of X st x in dom (f - g) holds
|.((f - g) . x).| < +infty let x be
Element of
X;
( x in dom (f - g) implies |.((f - g) . x).| < +infty )assume A208:
x in dom (f - g)
;
|.((f - g) . x).| < +infty
g is
real-valued
by A4, MESFUNC2:def 4;
then A209:
|.(g . x).| < +infty
by A5, A10, A208, MESFUNC2:def 1;
f is
real-valued
by A1, MESFUNC2:def 4;
then
|.(f . x).| < +infty
by A5, A10, A208, MESFUNC2:def 1;
then A210:
|.(f . x).| + |.(g . x).| <> +infty
by A209, XXREAL_3:16;
|.((f - g) . x).| = |.((f . x) - (g . x)).|
by A208, MESFUNC1:def 4;
then
|.((f - g) . x).| <= |.(f . x).| + |.(g . x).|
by EXTREAL1:32;
hence
|.((f - g) . x).| < +infty
by A210, XXREAL_0:2, XXREAL_0:4;
verum end;
then
f - g is real-valued
by MESFUNC2:def 1;
hence A211:
f - g is_simple_func_in S
by A5, A61, A10, A99, MESFUNC2:def 4; ( dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )
dom FG = dom a1
by A59, FINSEQ_1:def 3;
then
FG,a1 are_Re-presentation_of f
by A61, A123, MESFUNC3:def 1;
then A212:
integral (M,f) = Sum x1
by A1, A2, A3, A122, A155, MESFUNC4:3;
dom (z1 + y1) = Seg (len x1)
by A176, FINSEQ_1:def 3;
then
z1 + y1 is FinSequence
by FINSEQ_1:def 2;
then A213:
x1 = z1 + y1
by A176, A177, FINSEQ_1:13;
dom FG = dom b1
by A139, FINSEQ_1:def 3;
then
FG,b1 are_Re-presentation_of g
by A5, A61, A143, MESFUNC3:def 1;
then A214:
integral (M,g) = Sum y1
by A2, A4, A5, A6, A154, A164, MESFUNC4:3;
thus
dom (f - g) <> {}
by A2, A5, A10; ( f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )
for x being object st x in dom (f - g) holds
0 <= (f - g) . x
hence aa:
f - g is nonnegative
by SUPINF_2:52; integral (M,f) = (integral (M,(f - g))) + (integral (M,g))
dom FG = dom c1
by A140, FINSEQ_3:29;
then
FG,c1 are_Re-presentation_of f - g
by A5, A61, A10, A149, MESFUNC3:def 1;
then
integral (M,(f - g)) = Sum z1
by aa, A2, A5, A153, A156, A10, A211, MESFUNC4:3;
hence
integral (M,f) = (integral (M,(f - g))) + (integral (M,g))
by A164, A156, A212, A214, A213, MESFUNC4:1, ag, cd; verum