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 <> {} & 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; 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; 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; ( 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
; ( 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;
set la = len F;
A6:
dom f = union (rng F)
by A5, MESFUNC3:def 1;
consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that
A7:
G,b are_Re-presentation_of g
by A3, MESFUNC3:12;
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 for k being Nat st k in dom FG holds
FG . k in Sreconsider lb9 =
len G as
Nat ;
let k be
Nat;
( k in dom FG implies FG . k in S )set i =
((k -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
A11:
lb9 divides (len F) * (len G)
by NAT_D:def 3;
assume A12:
k in dom FG
;
FG . k in Sthen A13:
k in Seg ((len F) * (len G))
by A8, FINSEQ_1:def 3;
then A14:
k <= (len F) * (len G)
by FINSEQ_1:1;
then
k -' 1
<= ((len F) * (len G)) -' 1
by NAT_D:42;
then A15:
(k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G)
by NAT_2:24;
1
<= k
by A13, FINSEQ_1:1;
then A16:
1
<= (len F) * (len G)
by A14, XXREAL_0:2;
A17:
len G <> 0
by A13;
then
(k -' 1) mod (len G) < len G
by NAT_D:1;
then A18:
((k -' 1) mod (len G)) + 1
<= len G
by NAT_1:13;
len G >= 0 + 1
by A17, NAT_1:13;
then
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by A11, A16, NAT_2:15;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by A15, XREAL_1:19;
then A19:
((k -' 1) div (len G)) + 1
<= len F
by A17, NAT_D:18;
((k -' 1) div (len G)) + 1
>= 0 + 1
by XREAL_1:6;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A19;
then
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
then A20:
F . (((k -' 1) div (len G)) + 1) in rng F
by FUNCT_1:3;
((k -' 1) mod (len G)) + 1
>= 0 + 1
by XREAL_1:6;
then
((k -' 1) mod (len G)) + 1
in dom G
by A18, FINSEQ_3:25;
then A21:
G . (((k -' 1) mod (len G)) + 1) in rng G
by FUNCT_1:3;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A9, A12;
hence
FG . k in S
by A20, A21, MEASURE1:34;
verum end;
then reconsider FG = FG as FinSequence of S by Lm2;
A22:
for k, l being Nat st k in dom FG & l in dom FG & k <> l holds
FG . k misses FG . l
proof
A23:
len G divides (len F) * (len G)
by NAT_D:def 3;
let k,
l be
Nat;
( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )
assume that A24:
k in dom FG
and A25:
l in dom FG
and A26:
k <> l
;
FG . k misses FG . l
A27:
k in Seg ((len F) * (len G))
by A8, A24, FINSEQ_1:def 3;
then A28:
1
<= k
by FINSEQ_1:1;
set m =
((l -' 1) mod (len G)) + 1;
set n =
((l -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
set i =
((k -' 1) div (len G)) + 1;
A29:
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A9, A24;
A30:
k <= (len F) * (len G)
by A27, FINSEQ_1:1;
then A31:
1
<= (len F) * (len G)
by A28, XXREAL_0:2;
A32:
len G <> 0
by A27;
then
len G >= 0 + 1
by NAT_1:13;
then A33:
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by A23, A31, NAT_2:15;
A34:
l in Seg ((len F) * (len G))
by A8, A25, FINSEQ_1:def 3;
then A35:
1
<= l
by FINSEQ_1:1;
k -' 1
<= ((len F) * (len G)) -' 1
by A30, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A33, NAT_2:24;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:19;
then A40:
((k -' 1) div (len G)) + 1
<= len F
by A32, NAT_D:18;
((k -' 1) div (len G)) + 1
>= 0 + 1
by XREAL_1:6;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A40;
then A41:
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
A42:
((k -' 1) mod (len G)) + 1
>= 0 + 1
by XREAL_1:6;
(k -' 1) mod (len G) < len G
by A32, NAT_D:1;
then
((k -' 1) mod (len G)) + 1
<= len G
by NAT_1:13;
then A43:
((k -' 1) mod (len G)) + 1
in dom G
by A42, FINSEQ_3:25;
A44:
((l -' 1) mod (len G)) + 1
>= 0 + 1
by XREAL_1:6;
(l -' 1) mod (len G) < len G
by A32, NAT_D:1;
then
((l -' 1) mod (len G)) + 1
<= len G
by NAT_1:13;
then A45:
((l -' 1) mod (len G)) + 1
in dom G
by A44, FINSEQ_3:25;
A46:
((l -' 1) div (len G)) + 1
>= 0 + 1
by XREAL_1:6;
l <= (len F) * (len G)
by A34, FINSEQ_1:1;
then
l -' 1
<= ((len F) * (len G)) -' 1
by NAT_D:42;
then
(l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A33, NAT_2:24;
then
((l -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:19;
then
((l -' 1) div (len G)) + 1
<= len F
by A32, NAT_D:18;
then
((l -' 1) div (len G)) + 1
in Seg (len F)
by A46;
then A47:
((l -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
end;
A52:
g is real-valued
by A3, MESFUNC2:def 4;
then A53:
dom (f + g) = (dom f) /\ (dom g)
by MESFUNC2:2;
reconsider FG = FG as Finite_Sep_Sequence of S by A22, MESFUNC3:4;
A54:
dom g = union (rng G)
by A7, MESFUNC3:def 1;
A55:
dom f = union (rng FG)
proof
now for z being object st z in dom f holds
z in union (rng FG)let z be
object ;
( z in dom f implies z in union (rng FG) )assume A56:
z in dom f
;
z in union (rng FG)then consider Y being
set such that A57:
z in Y
and A58:
Y in rng F
by A6, TARSKI:def 4;
consider i being
Nat such that A59:
i in dom F
and A60:
Y = F . i
by A58, FINSEQ_2:10;
A61:
i in Seg (len F)
by A59, FINSEQ_1:def 3;
then
1
<= i
by FINSEQ_1:1;
then consider i9 being
Nat such that A62:
i = 1
+ i9
by NAT_1:10;
consider Z being
set such that A63:
z in Z
and A64:
Z in rng G
by A4, A54, A56, TARSKI:def 4;
consider j being
Nat such that A65:
j in dom G
and A66:
Z = G . j
by A64, FINSEQ_2:10;
A67:
j in Seg (len G)
by A65, FINSEQ_1:def 3;
then A68:
1
<= j
by FINSEQ_1:1;
then consider j9 being
Nat such that A69:
j = 1
+ j9
by NAT_1:10;
(i9 * (len G)) + j in NAT
by ORDINAL1:def 12;
then reconsider k =
((i - 1) * (len G)) + j as
Element of
NAT by A62;
i <= len F
by A61, FINSEQ_1:1;
then
i - 1
<= (len F) - 1
by XREAL_1:9;
then
(i - 1) * (len G) <= ((len F) - 1) * (len G)
by XREAL_1:64;
then A70:
k <= (((len F) - 1) * (len G)) + j
by XREAL_1:6;
A71:
j <= len G
by A67, FINSEQ_1:1;
then A72:
j9 < len G
by A69, NAT_1:13;
A73:
k >= 0 + j
by A62, XREAL_1:6;
then A74:
k -' 1 =
k - 1
by A68, XREAL_1:233, XXREAL_0:2
.=
(i9 * (len G)) + j9
by A62, A69
;
then A75:
i = ((k -' 1) div (len G)) + 1
by A62, A72, NAT_D:def 1;
(((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G)
by A71, XREAL_1:6;
then A76:
k <= (len F) * (len G)
by A70, XXREAL_0:2;
k >= 1
by A68, A73, XXREAL_0:2;
then A77:
k in Seg ((len F) * (len G))
by A76;
then
k in dom FG
by A8, FINSEQ_1:def 3;
then A78:
FG . k in rng FG
by FUNCT_1:def 3;
A79:
j = ((k -' 1) mod (len G)) + 1
by A69, A74, A72, NAT_D:def 2;
z in (F . i) /\ (G . j)
by A57, A60, A63, A66, XBOOLE_0:def 4;
then
z in FG . k
by A9, A10, A75, A79, A77;
hence
z in union (rng FG)
by A78, TARSKI:def 4;
verum end;
hence
dom f c= union (rng FG)
;
XBOOLE_0:def 10 union (rng FG) c= dom f
reconsider lb9 =
len G as
Nat ;
let z be
object ;
TARSKI:def 3 ( not z in union (rng FG) or z in dom f )
A80:
lb9 divides (len F) * (len G)
by NAT_D:def 3;
assume
z in union (rng FG)
;
z in dom f
then consider Y being
set such that A81:
z in Y
and A82:
Y in rng FG
by TARSKI:def 4;
consider k being
Nat such that A83:
k in dom FG
and A84:
Y = FG . k
by A82, FINSEQ_2:10;
A85:
k in Seg (len FG)
by A83, FINSEQ_1:def 3;
then A86:
k <= (len F) * (len G)
by A8, FINSEQ_1:1;
then A87:
k -' 1
<= ((len F) * (len G)) -' 1
by NAT_D:42;
set j =
((k -' 1) mod (len G)) + 1;
set i =
((k -' 1) div (len G)) + 1;
A88:
((k -' 1) div (len G)) + 1
>= 0 + 1
by NAT_1:13;
1
<= k
by A85, FINSEQ_1:1;
then A89:
1
<= (len F) * (len G)
by A86, XXREAL_0:2;
A90:
len G <> 0
by A8, A85;
then
len G >= 0 + 1
by NAT_1:13;
then
(((len F) * (len G)) -' 1) div lb9 = (((len F) * (len G)) div (len G)) - 1
by A80, A89, NAT_2:15;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A87, NAT_2:24;
then A91:
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:19;
((len F) * (len G)) div (len G) = len F
by A90, NAT_D:18;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A91, A88;
then
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
then A92:
F . (((k -' 1) div (len G)) + 1) in rng F
by FUNCT_1:def 3;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A9, A83;
then
z in F . (((k -' 1) div (len G)) + 1)
by A81, A84, XBOOLE_0:def 4;
hence
z in dom f
by A6, A92, TARSKI:def 4;
verum
end;
A93:
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
A94:
len G divides (len F) * (len G)
by NAT_D:def 3;
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 A95:
k in dom FG
and A96:
x in FG . k
and A97:
y in FG . k
;
(f + g) . x = (f + g) . y
set j =
((k -' 1) mod (len G)) + 1;
A98:
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A9, A95;
then A99:
y in G . (((k -' 1) mod (len G)) + 1)
by A97, XBOOLE_0:def 4;
set i =
((k -' 1) div (len G)) + 1;
A100:
((k -' 1) div (len G)) + 1
>= 0 + 1
by XREAL_1:6;
A101:
k in Seg (len FG)
by A95, FINSEQ_1:def 3;
then A102:
1
<= k
by FINSEQ_1:1;
A103:
len G > 0
by A8, A101;
then A104:
len G >= 0 + 1
by NAT_1:13;
A105:
k <= (len F) * (len G)
by A8, A101, FINSEQ_1:1;
then A106:
k -' 1
<= ((len F) * (len G)) -' 1
by NAT_D:42;
1
<= (len F) * (len G)
by A102, A105, XXREAL_0:2;
then
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by A104, A94, NAT_2:15;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A106, NAT_2:24;
then A107:
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:19;
len G <> 0
by A8, A101;
then
((k -' 1) div (len G)) + 1
<= len F
by A107, NAT_D:18;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A100;
then A108:
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
x in F . (((k -' 1) div (len G)) + 1)
by A96, A98, XBOOLE_0:def 4;
then A109:
f . x = a . (((k -' 1) div (len G)) + 1)
by A5, A108, MESFUNC3:def 1;
A110:
((k -' 1) mod (len G)) + 1
>= 0 + 1
by XREAL_1:6;
(k -' 1) mod (len G) < len G
by A103, 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 A110;
then A111:
((k -' 1) mod (len G)) + 1
in dom G
by FINSEQ_1:def 3;
y in F . (((k -' 1) div (len G)) + 1)
by A97, A98, XBOOLE_0:def 4;
then A112:
f . y = a . (((k -' 1) div (len G)) + 1)
by A5, A108, MESFUNC3:def 1;
A113:
FG . k in rng FG
by A95, FUNCT_1:def 3;
then
x in dom (f + g)
by A4, A55, A53, A96, TARSKI:def 4;
then A114:
(f + g) . x = (f . x) + (g . x)
by MESFUNC1:def 3;
x in G . (((k -' 1) mod (len G)) + 1)
by A96, A98, XBOOLE_0:def 4;
then
(f + g) . x = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1))
by A7, A109, A111, A114, MESFUNC3:def 1;
then A115:
(f + g) . x = (f . y) + (g . y)
by A7, A99, A111, A112, MESFUNC3:def 1;
y in dom (f + g)
by A4, A55, A53, A97, A113, TARSKI:def 4;
hence
(f + g) . x = (f + g) . y
by A115, 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 A116:
x in dom (f + g)
;
|.((f + g) . x).| < +infty then A117:
|.(g . x).| < +infty
by A4, A52, A53, MESFUNC2:def 1;
|.((f + g) . x).| = |.((f . x) + (g . x)).|
by A116, MESFUNC1:def 3;
then A118:
|.((f + g) . x).| <= |.(f . x).| + |.(g . x).|
by EXTREAL1:24;
f is
real-valued
by A1, MESFUNC2:def 4;
then
|.(f . x).| < +infty
by A4, A53, A116, MESFUNC2:def 1;
then
|.(f . x).| + |.(g . x).| <> +infty
by A117, XXREAL_3:16;
hence
|.((f + g) . x).| < +infty
by A118, XXREAL_0:2, XXREAL_0:4;
verum end;
then
f + g is real-valued
by MESFUNC2:def 1;
hence
f + g is_simple_func_in S
by A4, A55, A53, A93, MESFUNC2:def 4; dom (f + g) <> {}
thus
dom (f + g) <> {}
by A2, A4, A53; verum