let X be non empty set ; :: thesis: 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 <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
let f, g be PartFunc of X,ExtREAL ; :: thesis: ( f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f implies ( f + g is_simple_func_in S & dom (f + g) <> {} ) )
assume that
A1:
f is_simple_func_in S
and
A2:
dom f <> {}
and
A3:
g is_simple_func_in S
and
A4:
dom g = dom f
; :: thesis: ( f + g is_simple_func_in S & dom (f + g) <> {} )
consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A5:
F,a are_Re-presentation_of f
by A1, MESFUNC3:12;
consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that
A6:
G,b are_Re-presentation_of g
by A3, MESFUNC3:12;
A7:
( dom f = union (rng F) & dom g = union (rng G) )
by A5, A6, MESFUNC3:def 1;
set la = len F;
set lb = len G;
deffunc H1( Nat) -> set = (F . ((($1 -' 1) div (len G)) + 1)) /\ (G . ((($1 -' 1) mod (len G)) + 1));
consider FG being FinSequence such that
A8:
len FG = (len F) * (len G)
and
A9:
for k being Nat st k in dom FG holds
FG . k = H1(k)
from FINSEQ_1:sch 2();
A10:
dom FG = Seg ((len F) * (len G))
by A8, FINSEQ_1:def 3;
now let k be
Nat;
:: thesis: ( k in dom FG implies FG . k in S )assume A11:
k in dom FG
;
:: thesis: FG . k in Sthen A12:
k in Seg ((len F) * (len G))
by A8, FINSEQ_1:def 3;
A13:
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A9, A11;
set i =
((k -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
A14:
(
((k -' 1) div (len G)) + 1
>= 0 + 1 &
((k -' 1) mod (len G)) + 1
>= 0 + 1 )
by XREAL_1:8;
reconsider la' =
len F,
lb' =
len G as
natural number ;
A15:
( 1
<= k &
k <= (len F) * (len G) )
by A12, FINSEQ_1:3;
A16:
len G <> 0
by A12;
len G >= 0 + 1
by A16, NAT_1:13;
then
(
lb' divides (len F) * (len G) & 1
<= (len F) * (len G) & 1
<= len G )
by A15, NAT_D:def 3, XXREAL_0:2;
then A18:
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by NAT_2:17;
k -' 1
<= ((len F) * (len G)) -' 1
by A15, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G)
by NAT_2:26;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by A18, XREAL_1:21;
then
((k -' 1) div (len G)) + 1
<= len F
by A16, NAT_D:18;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A14;
then
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
then A19:
F . (((k -' 1) div (len G)) + 1) in rng F
by FUNCT_1:12;
(k -' 1) mod (len G) < len G
by A16, NAT_D:1;
then
((k -' 1) mod (len G)) + 1
<= len G
by NAT_1:13;
then
((k -' 1) mod (len G)) + 1
in dom G
by A14, FINSEQ_3:27;
then
G . (((k -' 1) mod (len G)) + 1) in rng G
by FUNCT_1:12;
hence
FG . k in S
by A13, A19, MEASURE1:66;
:: thesis: verum end;
then reconsider FG = FG as FinSequence of S by Lm3;
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;
:: thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )
assume A20:
(
k in dom FG &
l in dom FG &
k <> l )
;
:: thesis: FG . k misses FG . l
set i =
((k -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
set n =
((l -' 1) div (len G)) + 1;
set m =
((l -' 1) mod (len G)) + 1;
A21:
(
k in Seg ((len F) * (len G)) &
l in Seg ((len F) * (len G)) )
by A8, A20, FINSEQ_1:def 3;
A22:
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A9, A20;
A23:
(
((k -' 1) div (len G)) + 1
>= 0 + 1 &
((k -' 1) mod (len G)) + 1
>= 0 + 1 &
((l -' 1) div (len G)) + 1
>= 0 + 1 &
((l -' 1) mod (len G)) + 1
>= 0 + 1 )
by XREAL_1:8;
reconsider la' =
len F,
lb' =
len G as
natural number ;
A24:
( 1
<= k &
k <= (len F) * (len G) & 1
<= l &
l <= (len F) * (len G) )
by A21, FINSEQ_1:3;
A25:
len G <> 0
by A21;
len G >= 0 + 1
by A25, NAT_1:13;
then
(
len G divides (len F) * (len G) & 1
<= (len F) * (len G) & 1
<= len G )
by A24, NAT_D:def 3, XXREAL_0:2;
then A27:
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by NAT_2:17;
(
k -' 1
<= ((len F) * (len G)) -' 1 &
l -' 1
<= ((len F) * (len G)) -' 1 )
by A24, NAT_D:42;
then
(
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 &
(l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 )
by A27, NAT_2:26;
then
(
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G) &
((l -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G) )
by XREAL_1:21;
then
(
((k -' 1) div (len G)) + 1
<= len F &
((l -' 1) div (len G)) + 1
<= len F )
by A25, NAT_D:18;
then
(
((k -' 1) div (len G)) + 1
in Seg (len F) &
((l -' 1) div (len G)) + 1
in Seg (len F) )
by A23;
then A28:
(
((k -' 1) div (len G)) + 1
in dom F &
((l -' 1) div (len G)) + 1
in dom F )
by FINSEQ_1:def 3;
(
(k -' 1) mod (len G) < len G &
(l -' 1) mod (len G) < len G )
by A25, NAT_D:1;
then
(
((k -' 1) mod (len G)) + 1
<= len G &
((l -' 1) mod (len G)) + 1
<= len G )
by NAT_1:13;
then A29:
(
((k -' 1) mod (len G)) + 1
in dom G &
((l -' 1) mod (len G)) + 1
in dom G )
by A23, FINSEQ_3:27;
end;
then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A34:
dom f = union (rng FG)
proof
now let z be
set ;
:: thesis: ( z in dom f implies z in union (rng FG) )assume A35:
z in dom f
;
:: thesis: z in union (rng FG)then consider Y being
set such that A36:
(
z in Y &
Y in rng F )
by A7, TARSKI:def 4;
consider i being
Nat such that A37:
(
i in dom F &
Y = F . i )
by A36, FINSEQ_2:11;
i in Seg (len F)
by A37, FINSEQ_1:def 3;
then A38:
( 1
<= i &
i <= len F )
by FINSEQ_1:3;
then consider i' being
Nat such that A39:
i = 1
+ i'
by NAT_1:10;
consider Z being
set such that A40:
(
z in Z &
Z in rng G )
by A4, A7, A35, TARSKI:def 4;
consider j being
Nat such that A41:
(
j in dom G &
Z = G . j )
by A40, FINSEQ_2:11;
(i' * (len G)) + j is
Nat
;
then reconsider k =
((i - 1) * (len G)) + j as
Element of
NAT by A39;
j in Seg (len G)
by A41, FINSEQ_1:def 3;
then A42:
( 1
<= j &
j <= len G )
by FINSEQ_1:3;
then consider j' being
Nat such that A43:
j = 1
+ j'
by NAT_1:10;
A44:
k >= 0 + j
by A39, XREAL_1:8;
then A45:
k >= 1
by A42, XXREAL_0:2;
A46:
k -' 1 =
k - 1
by A42, A44, XREAL_1:235, XXREAL_0:2
.=
(i' * (len G)) + j'
by A39, A43
;
j' < len G
by A42, A43, NAT_1:13;
then A47:
(
i = ((k -' 1) div (len G)) + 1 &
j = ((k -' 1) mod (len G)) + 1 )
by A39, A43, A46, NAT_D:def 1, NAT_D:def 2;
i - 1
<= (len F) - 1
by A38, XREAL_1:11;
then
(i - 1) * (len G) <= ((len F) - 1) * (len G)
by XREAL_1:66;
then A48:
k <= (((len F) - 1) * (len G)) + j
by XREAL_1:8;
(((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G)
by A42, XREAL_1:8;
then
k <= (len F) * (len G)
by A48, XXREAL_0:2;
then A49:
k in Seg ((len F) * (len G))
by A45;
z in (F . i) /\ (G . j)
by A36, A37, A40, A41, XBOOLE_0:def 4;
then A50:
z in FG . k
by A9, A47, A49, A10;
k in dom FG
by A8, A49, FINSEQ_1:def 3;
then
FG . k in rng FG
by FUNCT_1:def 5;
hence
z in union (rng FG)
by A50, TARSKI:def 4;
:: thesis: verum end;
hence
dom f c= union (rng FG)
by TARSKI:def 3;
:: according to XBOOLE_0:def 10 :: thesis: union (rng FG) c= dom f
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in union (rng FG) or z in dom f )
assume
z in union (rng FG)
;
:: thesis: z in dom f
then consider Y being
set such that A51:
(
z in Y &
Y in rng FG )
by TARSKI:def 4;
consider k being
Nat such that A52:
(
k in dom FG &
Y = FG . k )
by A51, FINSEQ_2:11;
set i =
((k -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A9, A52;
then A53:
z in F . (((k -' 1) div (len G)) + 1)
by A51, A52, XBOOLE_0:def 4;
reconsider la' =
len F,
lb' =
len G as
natural number ;
X:
k in Seg (len FG)
by A52, FINSEQ_1:def 3;
then A54:
( 1
<= k &
k <= (len F) * (len G) )
by A8, FINSEQ_1:3;
A55:
len G <> 0
by X, A8;
then
len G >= 0 + 1
by NAT_1:13;
then
(
lb' divides (len F) * (len G) & 1
<= (len F) * (len G) & 1
<= len G )
by A54, NAT_D:def 3, XXREAL_0:2;
then A56:
(((len F) * (len G)) -' 1) div lb' = (((len F) * (len G)) div (len G)) - 1
by NAT_2:17;
k -' 1
<= ((len F) * (len G)) -' 1
by A54, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A56, NAT_2:26;
then A57:
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:21;
A58:
(
((k -' 1) div (len G)) + 1
>= 0 + 1 &
((k -' 1) mod (len G)) + 1
>= 0 + 1 )
by NAT_1:13;
((len F) * (len G)) div (len G) = len F
by A55, NAT_D:18;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A57, A58;
then
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
then
F . (((k -' 1) div (len G)) + 1) in rng F
by FUNCT_1:def 5;
hence
z in dom f
by A7, A53, TARSKI:def 4;
:: thesis: verum
end;
A59:
g is real-valued
by A3, MESFUNC2:def 5;
then A60:
dom (f + g) = (dom f) /\ (dom g)
by MESFUNC2:2;
now let x be
Element of
X;
:: thesis: ( x in dom (f + g) implies |.((f + g) . x).| < +infty )assume A61:
x in dom (f + g)
;
:: thesis: |.((f + g) . x).| < +infty then A62:
|.((f + g) . x).| = |.((f . x) + (g . x)).|
by MESFUNC1:def 3;
f is
real-valued
by A1, MESFUNC2:def 5;
then A63:
(
|.(f . x).| < +infty &
|.(g . x).| < +infty )
by A4, A59, A60, A61, MESFUNC2:def 1;
A64:
|.((f + g) . x).| <= |.(f . x).| + |.(g . x).|
by A62, A59, EXTREAL2:61;
|.(f . x).| + |.(g . x).| <> +infty
by A63, XXREAL_3:16;
hence
|.((f + g) . x).| < +infty
by A64, XXREAL_0:2, XXREAL_0:4;
:: thesis: verum end;
then A65:
f + g is real-valued
by MESFUNC2:def 1;
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;
:: thesis: 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;
:: thesis: ( k in dom FG & x in FG . k & y in FG . k implies (f + g) . x = (f + g) . y )
assume A66:
(
k in dom FG &
x in FG . k &
y in FG . k )
;
:: thesis: (f + g) . x = (f + g) . y
set i =
((k -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A9, A66;
then A67:
(
x in F . (((k -' 1) div (len G)) + 1) &
x in G . (((k -' 1) mod (len G)) + 1) &
y in F . (((k -' 1) div (len G)) + 1) &
y in G . (((k -' 1) mod (len G)) + 1) )
by A66, XBOOLE_0:def 4;
B68:
k in Seg (len FG)
by A66, FINSEQ_1:def 3;
then A68:
( 1
<= k &
k <= (len F) * (len G) )
by A8, FINSEQ_1:3;
A69:
(
((k -' 1) div (len G)) + 1
>= 0 + 1 &
((k -' 1) mod (len G)) + 1
>= 0 + 1 )
by XREAL_1:8;
A70:
len G <> 0
by B68, A8;
A71:
len G > 0
by A68;
then
len G >= 0 + 1
by NAT_1:13;
then
(
len G divides (len F) * (len G) & 1
<= (len F) * (len G) & 1
<= len G )
by A68, NAT_D:def 3, XXREAL_0:2;
then A72:
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by NAT_2:17;
k -' 1
<= ((len F) * (len G)) -' 1
by A68, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A72, NAT_2:26;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:21;
then
((k -' 1) div (len G)) + 1
<= len F
by A70, NAT_D:18;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A69;
then A73:
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
then A74:
f . x = a . (((k -' 1) div (len G)) + 1)
by A5, A67, MESFUNC3:def 1;
(k -' 1) mod (len G) < len G
by A71, NAT_D:1;
then
((k -' 1) mod (len G)) + 1
<= len G
by NAT_1:13;
then
((k -' 1) mod (len G)) + 1
in Seg (len G)
by A69;
then A75:
((k -' 1) mod (len G)) + 1
in dom G
by FINSEQ_1:def 3;
A76:
f . y = a . (((k -' 1) div (len G)) + 1)
by A5, A67, A73, MESFUNC3:def 1;
FG . k in rng FG
by A66, FUNCT_1:def 5;
then A77:
(
x in dom (f + g) &
y in dom (f + g) )
by A4, A34, A60, A66, TARSKI:def 4;
then
(f + g) . x = (f . x) + (g . x)
by MESFUNC1:def 3;
then
(f + g) . x = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1))
by A6, A67, A74, A75, MESFUNC3:def 1;
then
(f + g) . x = (f . y) + (g . y)
by A6, A67, A75, A76, MESFUNC3:def 1;
hence
(f + g) . x = (f + g) . y
by A77, MESFUNC1:def 3;
:: thesis: verum
end;
hence
f + g is_simple_func_in S
by A4, A34, A60, A65, MESFUNC2:def 5; :: thesis: dom (f + g) <> {}
thus
dom (f + g) <> {}
by A2, A4, A60; :: thesis: verum