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,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; :: thesis: 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; :: thesis: 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 ; :: 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) <> {} )
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;
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
A6:
G,b are_Re-presentation_of R_EAL g
by 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;
then A16:
len G <> 0
;
then A17:
len G > 0
;
then
len G >= 0 + 1
by NAT_1:13;
then
(
lb' divides la' * lb' & 1
<= (len F) * (len G) & 1
<= len G )
by A15, NAT_D:def 3, XXREAL_0:2;
then A18:
((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 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 A17, 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;
then
(
F . (((k -' 1) div (len G)) + 1) in S &
G . (((k -' 1) mod (len G)) + 1) in S )
by A19;
then
(F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S
by MEASURE1:66;
hence
FG . k in S
by A13;
:: thesis: verum end;
then reconsider FG = FG as FinSequence of S by FINSEQ_2:14;
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;
then A25:
len G <> 0
;
then A26:
len G > 0
;
then
len G >= 0 + 1
by NAT_1:13;
then
(
lb' divides la' * lb' & 1
<= (len F) * (len G) & 1
<= len G )
by A24, NAT_D:def 3, XXREAL_0:2;
then A27:
((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 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 A26, 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;
reconsider k =
((i - 1) * (len G)) + j as
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;
(
0 <= len G &
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, FINSEQ_1:3;
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 ;
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;
then A55:
len G <> 0
;
then
len G > 0
;
then
len G >= 0 + 1
by NAT_1:13;
then
(
lb' divides la' * lb' & 1
<= (len F) * (len G) & 1
<= len G )
by A54, NAT_D:def 3, XXREAL_0:2;
then A56:
((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 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 XREAL_1:8;
((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:
dom (f + g) = (dom f) /\ (dom g)
by VALUED_1: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 A60:
(
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, A60;
then A61:
(
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 A60, XBOOLE_0:def 4;
k in Seg (len FG)
by A60, FINSEQ_1:def 3;
then A62:
( 1
<= k &
k <= (len F) * (len G) )
by A8, FINSEQ_1:3;
A63:
(
((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 ;
A64:
len G <> 0
by A62;
then A65:
len G > 0
;
then
len G >= 0 + 1
by NAT_1:13;
then
(
lb' divides la' * lb' & 1
<= (len F) * (len G) & 1
<= len G )
by A62, NAT_D:def 3, XXREAL_0:2;
then A66:
((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 1
by NAT_2:17;
k -' 1
<= ((len F) * (len G)) -' 1
by A62, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A66, 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 A64, NAT_D:18;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A63;
then A67:
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
(k -' 1) mod (len G) < len G
by A65, 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 A63;
then A68:
((k -' 1) mod (len G)) + 1
in dom G
by FINSEQ_1:def 3;
FG . k in rng FG
by A60, FUNCT_1:def 5;
then A69:
(
x in dom (f + g) &
y in dom (f + g) )
by A4, A34, A59, A60, TARSKI:def 4;
(
f . x = a . (((k -' 1) div (len G)) + 1) &
g . x = b . (((k -' 1) mod (len G)) + 1) )
by A5, A6, A61, A67, A68, MESFUNC3:def 1;
then
(f . x) + (g . x) = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1))
by SUPINF_2:1;
then A70:
(f + g) . x = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1))
by A69, VALUED_1:def 1;
(
f . y = a . (((k -' 1) div (len G)) + 1) &
g . y = b . (((k -' 1) mod (len G)) + 1) )
by A5, A6, A61, A67, A68, MESFUNC3:def 1;
then
(f + g) . x = (f . y) + (g . y)
by A70, SUPINF_2:1;
hence
(f + g) . x = (f + g) . y
by A69, VALUED_1:def 1;
:: thesis: verum
end;
hence
f + g is_simple_func_in S
by A4, A34, A59, Def7; :: thesis: dom (f + g) <> {}
thus
dom (f + g) <> {}
by A2, A4, A59; :: thesis: verum