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,REAL 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,REAL 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,REAL 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,REAL; ( 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) <> {} )
R_EAL f is_simple_func_in S
by A1, Th49;
then consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A5:
F,a are_Re-presentation_of R_EAL f
by MESFUNC3:12;
set la = len F;
A6:
dom f = union (rng F)
by A5, MESFUNC3:def 1;
R_EAL g is_simple_func_in S
by A3, Th49;
then consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that
A7:
G,b are_Re-presentation_of R_EAL g
by MESFUNC3:12;
set lb = len G;
A8:
dom (f + g) = (dom f) /\ (dom g)
by VALUED_1:def 1;
deffunc H1( Nat) -> set = (F . ((($1 -' 1) div (len G)) + 1)) /\ (G . ((($1 -' 1) mod (len G)) + 1));
consider FG being FinSequence such that
A9:
len FG = (len F) * (len G)
and
A10:
for k being Nat st k in dom FG holds
FG . k = H1(k)
from FINSEQ_1:sch 2();
A11:
dom FG = Seg ((len F) * (len G))
by A9, FINSEQ_1:def 3;
now for k being Nat st k in dom FG holds
FG . k in Sreconsider la9 =
len F,
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;
assume A12:
k in dom FG
;
FG . k in Sthen A13:
k in Seg ((len F) * (len G))
by A9, 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:
(
lb9 divides la9 * lb9 & 1
<= (len F) * (len G) )
by A14, NAT_D:def 3, XXREAL_0:2;
A17:
len G <> 0
by A13, A14, FINSEQ_1:1;
then
len G >= 0 + 1
by NAT_1:13;
then
((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1
by A16, NAT_2:15;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by A15, XREAL_1:19;
then
(
((k -' 1) div (len G)) + 1
>= 0 + 1 &
((k -' 1) div (len G)) + 1
<= len F )
by A17, NAT_D:18, XREAL_1:6;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
;
then
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
then A18:
F . (((k -' 1) div (len G)) + 1) in rng F
by FUNCT_1:3;
(k -' 1) mod (len G) < len G
by A17, NAT_D:1;
then
(
((k -' 1) mod (len G)) + 1
>= 0 + 1 &
((k -' 1) mod (len G)) + 1
<= len G )
by NAT_1:13;
then
((k -' 1) mod (len G)) + 1
in dom G
by FINSEQ_3:25;
then
G . (((k -' 1) mod (len G)) + 1) in rng G
by FUNCT_1:3;
then
(F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S
by A18, MEASURE1:34;
hence
FG . k in S
by A10, A12;
verum end;
then reconsider FG = FG as FinSequence of S by FINSEQ_2:12;
for k, l being Nat st k in dom FG & l in dom FG & k <> l holds
FG . k misses FG . l
proof
reconsider la9 =
len F,
lb9 =
len G as
Nat ;
let k,
l be
Nat;
( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )
assume that A19:
k in dom FG
and A20:
l in dom FG
and A21:
k <> l
;
FG . k misses FG . l
set j =
((k -' 1) mod (len G)) + 1;
set i =
((k -' 1) div (len G)) + 1;
A22:
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A10, A19;
set m =
((l -' 1) mod (len G)) + 1;
set n =
((l -' 1) div (len G)) + 1;
A23:
k in Seg ((len F) * (len G))
by A9, A19, FINSEQ_1:def 3;
then A24:
1
<= k
by FINSEQ_1:1;
then A25:
len G <> 0
by A23, FINSEQ_1:1;
then
(k -' 1) mod (len G) < len G
by NAT_D:1;
then
(
((k -' 1) mod (len G)) + 1
>= 0 + 1 &
((k -' 1) mod (len G)) + 1
<= len G )
by NAT_1:13;
then A26:
((k -' 1) mod (len G)) + 1
in dom G
by FINSEQ_3:25;
A27:
k <= (len F) * (len G)
by A23, FINSEQ_1:1;
then A28:
(
lb9 divides la9 * lb9 & 1
<= (len F) * (len G) )
by A24, NAT_D:def 3, XXREAL_0:2;
len G >= 0 + 1
by A25, NAT_1:13;
then A29:
((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1
by A28, NAT_2:15;
A30:
l in Seg ((len F) * (len G))
by A9, A20, FINSEQ_1:def 3;
then A31:
1
<= l
by FINSEQ_1:1;
k -' 1
<= ((len F) * (len G)) -' 1
by A27, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A29, NAT_2:24;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:19;
then
(
((k -' 1) div (len G)) + 1
>= 0 + 1 &
((k -' 1) div (len G)) + 1
<= len F )
by A25, NAT_D:18, XREAL_1:6;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
;
then A35:
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
(l -' 1) mod (len G) < len G
by A25, NAT_D:1;
then
(
((l -' 1) mod (len G)) + 1
>= 0 + 1 &
((l -' 1) mod (len G)) + 1
<= len G )
by NAT_1:13;
then A36:
((l -' 1) mod (len G)) + 1
in dom G
by FINSEQ_3:25;
l <= (len F) * (len G)
by A30, 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 A29, 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
>= 0 + 1 &
((l -' 1) div (len G)) + 1
<= len F )
by A25, NAT_D:18, XREAL_1:6;
then
((l -' 1) div (len G)) + 1
in Seg (len F)
;
then A37:
((l -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
end;
then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A42:
dom g = union (rng G)
by A7, MESFUNC3:def 1;
A43:
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 A44:
z in dom f
;
z in union (rng FG)then consider Y being
set such that A45:
z in Y
and A46:
Y in rng F
by A6, TARSKI:def 4;
consider i being
Nat such that A47:
i in dom F
and A48:
Y = F . i
by A46, FINSEQ_2:10;
A49:
i in Seg (len F)
by A47, FINSEQ_1:def 3;
then
1
<= i
by FINSEQ_1:1;
then consider i9 being
Nat such that A50:
i = 1
+ i9
by NAT_1:10;
consider Z being
set such that A51:
z in Z
and A52:
Z in rng G
by A4, A42, A44, TARSKI:def 4;
consider j being
Nat such that A53:
j in dom G
and A54:
Z = G . j
by A52, FINSEQ_2:10;
A55:
j in Seg (len G)
by A53, FINSEQ_1:def 3;
then A56:
1
<= j
by FINSEQ_1:1;
then consider j9 being
Nat such that A57:
j = 1
+ j9
by NAT_1:10;
A58:
j <= len G
by A55, FINSEQ_1:1;
then A59:
j9 < len G
by A57, NAT_1:13;
reconsider k =
((i - 1) * (len G)) + j as
Nat by A50;
A60:
k >= 0 + j
by A50, XREAL_1:6;
then A61:
k -' 1 =
k - 1
by A56, XREAL_1:233, XXREAL_0:2
.=
(i9 * (len G)) + j9
by A50, A57
;
then A62:
i = ((k -' 1) div (len G)) + 1
by A50, A59, NAT_D:def 1;
i <= len F
by A49, 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 A63:
k <= (((len F) - 1) * (len G)) + j
by XREAL_1:6;
(((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G)
by A58, XREAL_1:6;
then A64:
k <= (len F) * (len G)
by A63, XXREAL_0:2;
k >= 1
by A56, A60, XXREAL_0:2;
then A65:
k in Seg ((len F) * (len G))
by A64;
then
k in dom FG
by A9, FINSEQ_1:def 3;
then A66:
FG . k in rng FG
by FUNCT_1:def 3;
A67:
j = ((k -' 1) mod (len G)) + 1
by A57, A61, A59, NAT_D:def 2;
z in (F . i) /\ (G . j)
by A45, A48, A51, A54, XBOOLE_0:def 4;
then
z in FG . k
by A10, A11, A62, A67, A65;
hence
z in union (rng FG)
by A66, TARSKI:def 4;
verum end;
hence
dom f c= union (rng FG)
;
XBOOLE_0:def 10 union (rng FG) c= dom f
reconsider la9 =
len F,
lb9 =
len G as
Nat ;
let z be
object ;
TARSKI:def 3 ( not z in union (rng FG) or z in dom f )
assume
z in union (rng FG)
;
z in dom f
then consider Y being
set such that A68:
z in Y
and A69:
Y in rng FG
by TARSKI:def 4;
consider k being
Nat such that A70:
k in dom FG
and A71:
Y = FG . k
by A69, FINSEQ_2:10;
set j =
((k -' 1) mod (len G)) + 1;
set i =
((k -' 1) div (len G)) + 1;
A72:
k in Seg (len FG)
by A70, FINSEQ_1:def 3;
then A73:
k <= (len F) * (len G)
by A9, FINSEQ_1:1;
then A74:
len G <> 0
by A72, FINSEQ_1:1;
then A75:
len G >= 0 + 1
by NAT_1:13;
1
<= k
by A72, FINSEQ_1:1;
then
(
lb9 divides la9 * lb9 & 1
<= (len F) * (len G) )
by A73, NAT_D:def 3, XXREAL_0:2;
then A76:
((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1
by A75, NAT_2:15;
k -' 1
<= ((len F) * (len G)) -' 1
by A73, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A76, NAT_2:24;
then A77:
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:19;
(
((k -' 1) div (len G)) + 1
>= 0 + 1 &
((len F) * (len G)) div (len G) = len F )
by A74, NAT_D:18, XREAL_1:6;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A77;
then
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
then A78:
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 A10, A70;
then
z in F . (((k -' 1) div (len G)) + 1)
by A68, A71, XBOOLE_0:def 4;
hence
z in dom f
by A6, A78, TARSKI:def 4;
verum
end;
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
reconsider la9 =
len F,
lb9 =
len G as
Nat ;
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 A79:
k in dom FG
and A80:
x in FG . k
and A81:
y in FG . k
;
(f + g) . x = (f + g) . y
set i =
((k -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
A82:
k in Seg (len FG)
by A79, FINSEQ_1:def 3;
then A83:
k <= (len F) * (len G)
by A9, FINSEQ_1:1;
then A84:
k -' 1
<= ((len F) * (len G)) -' 1
by NAT_D:42;
A85:
len G <> 0
by A82, A83, FINSEQ_1:1;
then
(k -' 1) mod (len G) < len G
by NAT_D:1;
then
(
((k -' 1) mod (len G)) + 1
>= 0 + 1 &
((k -' 1) mod (len G)) + 1
<= len G )
by NAT_1:13;
then
((k -' 1) mod (len G)) + 1
in Seg (len G)
;
then A86:
((k -' 1) mod (len G)) + 1
in dom G
by FINSEQ_1:def 3;
1
<= k
by A82, FINSEQ_1:1;
then A87:
(
lb9 divides la9 * lb9 & 1
<= (len F) * (len G) )
by A83, NAT_D:def 3, XXREAL_0:2;
len G >= 0 + 1
by A85, NAT_1:13;
then
((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1
by A87, NAT_2:15;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A84, NAT_2:24;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:19;
then
(
((k -' 1) div (len G)) + 1
>= 0 + 1 &
((k -' 1) div (len G)) + 1
<= len F )
by A85, NAT_D:18, XREAL_1:6;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
;
then A88:
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
A89:
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A10, A79;
then
x in G . (((k -' 1) mod (len G)) + 1)
by A80, XBOOLE_0:def 4;
then A90:
g . x = b . (((k -' 1) mod (len G)) + 1)
by A7, A86, MESFUNC3:def 1;
y in G . (((k -' 1) mod (len G)) + 1)
by A81, A89, XBOOLE_0:def 4;
then A91:
g . y = b . (((k -' 1) mod (len G)) + 1)
by A7, A86, MESFUNC3:def 1;
x in F . (((k -' 1) div (len G)) + 1)
by A80, A89, XBOOLE_0:def 4;
then
f . x = a . (((k -' 1) div (len G)) + 1)
by A5, A88, MESFUNC3:def 1;
then A92:
(f . x) + (g . x) = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1))
by A90;
y in F . (((k -' 1) div (len G)) + 1)
by A81, A89, XBOOLE_0:def 4;
then A93:
f . y = a . (((k -' 1) div (len G)) + 1)
by A5, A88, MESFUNC3:def 1;
A94:
FG . k in rng FG
by A79, FUNCT_1:def 3;
then
x in dom (f + g)
by A4, A43, A8, A80, TARSKI:def 4;
then
(f + g) . x = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1))
by A92, VALUED_1:def 1;
then A95:
(f + g) . x = (f . y) + (g . y)
by A93, A91;
y in dom (f + g)
by A4, A43, A8, A81, A94, TARSKI:def 4;
hence
(f + g) . x = (f + g) . y
by A95, VALUED_1:def 1;
verum
end;
hence
f + g is_simple_func_in S
by A4, A43, A8; dom (f + g) <> {}
thus
dom (f + g) <> {}
by A2, A4, A8; verum