let X be non empty set ; for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & ex x being set st
( x in dom f & 0. = f . x ) holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) )
let S be SigmaField of X; for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & ex x being set st
( x in dom f & 0. = f . x ) holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) )
let f be PartFunc of X,ExtREAL; ( f is_simple_func_in S & f is nonnegative & ex x being set st
( x in dom f & 0. = f . x ) implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) ) )
assume that
A1:
f is_simple_func_in S
and
A2:
f is nonnegative
and
A3:
ex x being set st
( x in dom f & 0. = f . x )
; ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) )
a2:
for x being object st x in dom f holds
0. <= f . x
by A2, SUPINF_2:39;
consider x0 being set such that
A4:
x0 in dom f
and
A5:
0. = f . x0
by A3;
reconsider x0 = x0 as Element of X by A4;
consider F1 being Finite_Sep_Sequence of S such that
A6:
dom f = union (rng F1)
and
A7:
for n being Nat
for x, y being Element of X st n in dom F1 & x in F1 . n & y in F1 . n holds
f . x = f . y
by A1, MESFUNC2:def 4;
consider V being set such that
A8:
x0 in V
and
A9:
V in rng F1
by A4, A6, TARSKI:def 4;
consider n0 being object such that
A10:
n0 in dom F1
and
A11:
V = F1 . n0
by A9, FUNCT_1:def 3;
set F0 = { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } ;
set G1 = union { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } ;
for F9 being object st F9 in { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } holds
F9 in bool X
then reconsider F0 = { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } as Subset-Family of X by TARSKI:def 3;
set N = { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds
f . x = 0. ) ) } ;
A12:
len F1 <= (len F1) + 1
by NAT_1:11;
reconsider n0 = n0 as Element of NAT by A10;
( F1 . n0 is Element of S & F1 . n0 in rng F1 & ( for x being Element of X st x in F1 . n0 holds
f . x = 0. ) )
then A13:
F1 . n0 in F0
;
for z being object st z in F0 holds
z in rng F1
then A14:
F0 c= rng F1
;
for z being object st z in { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds
f . x = 0. ) ) } holds
z in dom F1
then A15:
{ n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds
f . x = 0. ) ) } c= dom F1
;
then reconsider N = { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds
f . x = 0. ) ) } as finite set ;
consider P1 being FinSequence such that
A16:
( rng P1 = N & P1 is one-to-one )
by FINSEQ_4:58;
reconsider F0 = F0 as N_Sub_set_fam of X by A14, A13;
for F9 being object st F9 in F0 holds
F9 in S
then
F0 c= S
;
then reconsider G1 = union { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } as Element of S by MEASURE1:def 5;
A17:
len P1 = card N
by A16, FINSEQ_4:62;
reconsider L = Seg (len F1) as finite set ;
set M = (findom F1) \ N;
consider P2 being FinSequence such that
A18:
rng P2 = (findom F1) \ N
and
A19:
P2 is one-to-one
by FINSEQ_4:58;
A20:
N c= Seg (len F1)
by A15, FINSEQ_1:def 3;
then
card N <= card L
by NAT_1:43;
then
len P1 <= len F1
by A17, FINSEQ_1:57;
then consider lenF being Nat such that
A21:
(len F1) + 1 = (len P1) + lenF
by A12, NAT_1:10, XXREAL_0:2;
reconsider lenF = lenF as Element of NAT by ORDINAL1:def 12;
(findom F1) \ N = (Seg (len F1)) \ N
by FINSEQ_1:def 3;
then A22:
card ((findom F1) \ N) = (card (Seg (len F1))) - (card N)
by A20, CARD_2:44;
defpred S1[ Nat, set ] means ( ( $1 = 1 implies $2 = G1 ) & ( $1 >= 2 implies ex k9 being Nat st
( k9 = $1 - 1 & $2 = F1 . (P2 . k9) ) ) );
len P2 = card ((findom F1) \ N)
by A18, A19, FINSEQ_4:62;
then A23:
len P2 = (((len F1) - (len P1)) + 1) - 1
by A17, A22, FINSEQ_1:57;
A24:
for k being Nat st k in Seg lenF holds
ex U being Element of S st S1[k,U]
proof
let k be
Nat;
( k in Seg lenF implies ex U being Element of S st S1[k,U] )
assume A25:
k in Seg lenF
;
ex U being Element of S st S1[k,U]
per cases
( k = 1 or k <> 1 )
;
suppose A26:
k = 1
;
ex U being Element of S st S1[k,U]take
G1
;
S1[k,G1]thus
S1[
k,
G1]
by A26;
verum end; suppose A27:
k <> 1
;
ex U being Element of S st S1[k,U]A28:
k >= 1
by A25, FINSEQ_1:1;
then consider k9 being
Nat such that A29:
k = 1
+ k9
by NAT_1:10;
k > 1
by A27, A28, XXREAL_0:1;
then
k >= 1
+ 1
by NAT_1:13;
then A30:
k - 1
>= 1
by XREAL_1:19;
k <= lenF
by A25, FINSEQ_1:1;
then
k - 1
<= lenF - 1
by XREAL_1:9;
then
k9 in Seg (len P2)
by A21, A23, A29, A30, FINSEQ_1:1;
then
k9 in dom P2
by FINSEQ_1:def 3;
then
P2 . k9 in (findom F1) \ N
by A18, FUNCT_1:3;
then
F1 . (P2 . k9) in rng F1
by FUNCT_1:3;
then reconsider U =
F1 . (P2 . k9) as
Element of
S ;
take
U
;
S1[k,U]thus
S1[
k,
U]
by A27, A29;
verum end; end;
end;
consider F being FinSequence of S such that
A31:
( dom F = Seg lenF & ( for k being Nat st k in Seg lenF holds
S1[k,F . k] ) )
from FINSEQ_1:sch 5(A24);
defpred S2[ Nat, Element of ExtREAL ] means for y being Element of X holds
( ( y in F . $1 implies $2 = f . y ) & ( F . $1 = {} implies $2 = 1. ) );
A32:
for k being Nat st k in Seg (len F) holds
ex x being Element of ExtREAL st S2[k,x]
proof
let k be
Nat;
( k in Seg (len F) implies ex x being Element of ExtREAL st S2[k,x] )
assume A33:
k in Seg (len F)
;
ex x being Element of ExtREAL st S2[k,x]
then A34:
k in dom F
by FINSEQ_1:def 3;
now ( ( k = 1 & ex x being Element of ExtREAL ex x being Element of ExtREAL st S2[k,x] ) or ( k <> 1 & ex x being Element of ExtREAL st S2[k,x] ) )per cases
( k = 1 or k <> 1 )
;
case A39:
k <> 1
;
ex x being Element of ExtREAL st S2[k,x]
1
<= k
by A33, FINSEQ_1:1;
then
1
< k
by A39, XXREAL_0:1;
then A40:
1
+ 1
<= k
by NAT_1:13;
then consider k1 being
Nat such that A41:
k1 = k - 1
and A42:
F . k = F1 . (P2 . k1)
by A31, A34;
A43:
1
<= k1
by A40, A41, XREAL_1:19;
k <= lenF
by A31, A34, FINSEQ_1:1;
then
k1 <= len P2
by A21, A23, A41, XREAL_1:9;
then
k1 in Seg (len P2)
by A43, FINSEQ_1:1;
then
k1 in dom P2
by FINSEQ_1:def 3;
then
P2 . k1 in (findom F1) \ N
by A18, FUNCT_1:3;
then consider k9 being
set such that A44:
k9 in dom F1
and A45:
F . k = F1 . k9
by A42;
hence
ex
x being
Element of
ExtREAL st
S2[
k,
x]
;
verum end; end; end;
hence
ex
x being
Element of
ExtREAL st
S2[
k,
x]
;
verum
end;
consider a being FinSequence of ExtREAL such that
A48:
( dom a = Seg (len F) & ( for n being Nat st n in Seg (len F) holds
S2[n,a . n] ) )
from FINSEQ_1:sch 5(A32);
A49:
for n being Nat
for x being Element of X st n in dom F & x in F . n holds
a . n = f . x
A52:
for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n
A55:
for x being Element of X st x in F1 . n0 holds
f . x = 0.
by A5, A7, A8, A10, A11;
A56:
( a . 1 = 0. & dom F = dom a & ( for n being Nat
for x being Element of X st n in dom F & x in F . n holds
a . n = f . x ) )
proof
reconsider F1n0 =
F1 . n0 as
Element of
S by A9, A11;
0 + 1
<= lenF
by A21, A23, XREAL_1:19;
then A57:
1
in Seg lenF
by FINSEQ_1:1;
then A58:
1
in Seg (len F)
by A31, FINSEQ_1:def 3;
A59:
F . 1
= G1
by A31, A57;
F1n0 in F0
by A9, A11, A55;
then
x0 in F . 1
by A8, A11, A59, TARSKI:def 4;
hence
a . 1
= 0.
by A5, A48, A58;
( dom F = dom a & ( for n being Nat
for x being Element of X st n in dom F & x in F . n holds
a . n = f . x ) )
thus
dom F = dom a
by A48, FINSEQ_1:def 3;
for n being Nat
for x being Element of X st n in dom F & x in F . n holds
a . n = f . x
thus
for
n being
Nat for
x being
Element of
X st
n in dom F &
x in F . n holds
a . n = f . x
by A49;
verum
end;
A60:
for n, m being Nat st n in dom F & m in dom F & n = 1 & m <> 1 holds
F . n misses F . m
proof
let n,
m be
Nat;
( n in dom F & m in dom F & n = 1 & m <> 1 implies F . n misses F . m )
assume that A61:
n in dom F
and A62:
m in dom F
and A63:
n = 1
and A64:
m <> 1
;
F . n misses F . m
A65:
F . n = G1
by A31, A61, A63;
m <= lenF
by A31, A62, FINSEQ_1:1;
then A66:
m - 1
<= lenF - 1
by XREAL_1:9;
1
<= m
by A62, FINSEQ_3:25;
then
1
< m
by A64, XXREAL_0:1;
then A67:
1
+ 1
<= m
by NAT_1:13;
then consider k9 being
Nat such that A68:
k9 = m - 1
and A69:
F . m = F1 . (P2 . k9)
by A31, A62;
m - 1
>= 1
by A67, XREAL_1:19;
then
k9 in Seg (len P2)
by A21, A23, A68, A66, FINSEQ_1:1;
then
k9 in dom P2
by FINSEQ_1:def 3;
then A70:
P2 . k9 in (findom F1) \ N
by A18, FUNCT_1:3;
then A71:
not
P2 . k9 in N
by XBOOLE_0:def 5;
(F . n) /\ (F . m) = {}
proof
assume
(F . n) /\ (F . m) <> {}
;
contradiction
then consider v being
object such that A72:
v in (F . n) /\ (F . m)
by XBOOLE_0:def 1;
A73:
v in F . m
by A72, XBOOLE_0:def 4;
v in F . n
by A72, XBOOLE_0:def 4;
then consider Y being
set such that A74:
v in Y
and A75:
Y in F0
by A65, TARSKI:def 4;
consider Fv being
Element of
S such that A76:
Y = Fv
and A77:
Fv in rng F1
and A78:
for
x being
Element of
X st
x in Fv holds
f . x = 0.
by A75;
consider n9 being
object such that A79:
n9 in dom F1
and A80:
Fv = F1 . n9
by A77, FUNCT_1:def 3;
reconsider n9 =
n9 as
Element of
NAT by A79;
n9 <> P2 . k9
by A70, A71, A78, A80;
then
F1 . n9 misses F1 . (P2 . k9)
by PROB_2:def 2;
then
(F1 . n9) /\ (F1 . (P2 . k9)) = {}
;
hence
contradiction
by A69, A73, A74, A76, A80, XBOOLE_0:def 4;
verum
end;
hence
F . n misses F . m
;
verum
end;
A81:
for n, m being Nat st n in dom F & m in dom F & n <> 1 & m <> 1 & n <> m holds
F . n misses F . m
proof
let n,
m be
Nat;
( n in dom F & m in dom F & n <> 1 & m <> 1 & n <> m implies F . n misses F . m )
assume that A82:
n in dom F
and A83:
m in dom F
and A84:
n <> 1
and A85:
m <> 1
and A86:
n <> m
;
F . n misses F . m
n <= lenF
by A31, A82, FINSEQ_1:1;
then A87:
n - 1
<= lenF - 1
by XREAL_1:9;
m <= lenF
by A31, A83, FINSEQ_1:1;
then A88:
m - 1
<= lenF - 1
by XREAL_1:9;
1
<= m
by A31, A83, FINSEQ_1:1;
then
1
< m
by A85, XXREAL_0:1;
then A89:
1
+ 1
<= m
by NAT_1:13;
then consider k2 being
Nat such that A90:
k2 = m - 1
and A91:
F . m = F1 . (P2 . k2)
by A31, A83;
1
<= m - 1
by A89, XREAL_1:19;
then
k2 in Seg (len P2)
by A21, A23, A90, A88, FINSEQ_1:1;
then A92:
k2 in dom P2
by FINSEQ_1:def 3;
1
<= n
by A31, A82, FINSEQ_1:1;
then
1
< n
by A84, XXREAL_0:1;
then A93:
1
+ 1
<= n
by NAT_1:13;
then consider k1 being
Nat such that A94:
k1 = n - 1
and A95:
F . n = F1 . (P2 . k1)
by A31, A82;
1
<= n - 1
by A93, XREAL_1:19;
then
k1 in Seg (len P2)
by A21, A23, A94, A87, FINSEQ_1:1;
then A96:
k1 in dom P2
by FINSEQ_1:def 3;
k1 <> k2
by A86, A94, A90;
then
P2 . k1 <> P2 . k2
by A19, A96, A92, FUNCT_1:def 4;
hence
F . n misses F . m
by A95, A91, PROB_2:def 2;
verum
end;
A97:
for x, y being object st x <> y holds
F . x misses F . y
for z being object st z in union (rng F) holds
z in union (rng F1)
proof
let z be
object ;
( z in union (rng F) implies z in union (rng F1) )
assume
z in union (rng F)
;
z in union (rng F1)
then consider Y being
set such that A101:
z in Y
and A102:
Y in rng F
by TARSKI:def 4;
consider k being
object such that A103:
k in dom F
and A104:
Y = F . k
by A102, FUNCT_1:def 3;
reconsider k =
k as
Element of
NAT by A103;
now ( ( k = 1 & z in union (rng F1) ) or ( k <> 1 & z in union (rng F1) ) )per cases
( k = 1 or k <> 1 )
;
case A107:
k <> 1
;
z in union (rng F1)
1
<= k
by A31, A103, FINSEQ_1:1;
then
1
< k
by A107, XXREAL_0:1;
then A108:
1
+ 1
<= k
by NAT_1:13;
then consider k9 being
Nat such that A109:
k9 = k - 1
and A110:
F . k = F1 . (P2 . k9)
by A31, A103;
A111:
1
<= k9
by A108, A109, XREAL_1:19;
k <= lenF
by A31, A103, FINSEQ_1:1;
then
k9 <= len P2
by A21, A23, A109, XREAL_1:9;
then
k9 in dom P2
by A111, FINSEQ_3:25;
then
P2 . k9 in (findom F1) \ N
by A18, FUNCT_1:3;
then
F1 . (P2 . k9) in rng F1
by FUNCT_1:3;
hence
z in union (rng F1)
by A101, A104, A110, TARSKI:def 4;
verum end; end; end;
hence
z in union (rng F1)
;
verum
end;
then A112:
union (rng F) c= union (rng F1)
;
for z being object st z in union (rng F1) holds
z in union (rng F)
proof
let z be
object ;
( z in union (rng F1) implies z in union (rng F) )
assume
z in union (rng F1)
;
z in union (rng F)
then consider Y being
set such that A113:
z in Y
and A114:
Y in rng F1
by TARSKI:def 4;
consider m1 being
object such that A115:
m1 in dom F1
and A116:
Y = F1 . m1
by A114, FUNCT_1:def 3;
reconsider m1 =
m1 as
Element of
NAT by A115;
now ( ( m1 in N & z in union (rng F) ) or ( not m1 in N & z in union (rng F) ) )per cases
( m1 in N or not m1 in N )
;
case
not
m1 in N
;
z in union (rng F)then
m1 in (findom F1) \ N
by A115, XBOOLE_0:def 5;
then consider m19 being
object such that A119:
m19 in dom P2
and A120:
m1 = P2 . m19
by A18, FUNCT_1:def 3;
reconsider m19 =
m19 as
Element of
NAT by A119;
A121:
m19 in Seg (len P2)
by A119, FINSEQ_1:def 3;
then
m19 <= len P2
by FINSEQ_1:1;
then A122:
m19 + 1
<= lenF
by A21, A23, XREAL_1:6;
reconsider m2 =
m19 + 1 as
Nat ;
1
<= m19
by A121, FINSEQ_1:1;
then A123:
1
+ 1
<= m19 + 1
by XREAL_1:6;
then
1
<= m2
by XXREAL_0:2;
then A124:
m2 in Seg lenF
by A122, FINSEQ_1:1;
then A125:
F . m2 in rng F
by A31, FUNCT_1:3;
ex
k9 being
Nat st
(
k9 = m2 - 1 &
F . m2 = F1 . (P2 . k9) )
by A31, A123, A124;
hence
z in union (rng F)
by A113, A116, A120, A125, TARSKI:def 4;
verum end; end; end;
hence
z in union (rng F)
;
verum
end;
then
union (rng F1) c= union (rng F)
;
then A126:
union (rng F) = dom f
by A6, A112;
reconsider F = F as Finite_Sep_Sequence of S by A97, PROB_2:def 2;
take
F
; ex a being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) )
take
a
; ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) )
for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty )
proof
A127:
f is
V77()
by A1, MESFUNC2:def 4;
0 + 1
<= lenF
by A21, A23, XREAL_1:19;
then A128:
1
in dom F
by A31, FINSEQ_1:1;
let n be
Nat;
( 2 <= n & n in dom a implies ( 0. < a . n & a . n < +infty ) )
assume that A129:
2
<= n
and A130:
n in dom a
;
( 0. < a . n & a . n < +infty )
1
+ 1
<= n
by A129;
then A131:
1
<= n - 1
by XREAL_1:19;
consider k1 being
Nat such that A132:
k1 = n - 1
and A133:
F . n = F1 . (P2 . k1)
by A31, A56, A129, A130;
n <= lenF
by A31, A56, A130, FINSEQ_1:1;
then
n - 1
<= lenF - 1
by XREAL_1:9;
then
k1 in Seg (len P2)
by A21, A23, A132, A131, FINSEQ_1:1;
then
k1 in dom P2
by FINSEQ_1:def 3;
then
P2 . k1 in (findom F1) \ N
by A18, FUNCT_1:3;
then A134:
F . n in rng F1
by A133, FUNCT_1:3;
n <> 1
by A129;
then
F . 1
misses F . n
by A56, A60, A130, A128;
then A135:
G1 misses F . n
by A31, A128;
(
a . n <> 0. &
0. <= a . n &
a . n < +infty )
proof
per cases
( F . n <> {} or F . n = {} )
;
suppose A136:
F . n <> {}
;
( a . n <> 0. & 0. <= a . n & a . n < +infty )A137:
F . n in rng F
by A56, A130, FUNCT_1:3;
then reconsider Fn =
F . n as
Element of
S ;
consider y being
object such that A138:
y in F . n
by A136, XBOOLE_0:def 1;
F . n in S
by A137;
then reconsider y =
y as
Element of
X by A138;
A139:
a . n = f . y
by A48, A130, A138;
G1 /\ (F . n) = {}
by A135;
then A140:
not
y in G1
by A138, XBOOLE_0:def 4;
thus
a . n <> 0.
( 0. <= a . n & a . n < +infty )A141:
y in union (rng F)
by A138, A137, TARSKI:def 4;
then
|.(f . y).| < +infty
by A6, A112, A127, MESFUNC2:def 1;
hence
(
0. <= a . n &
a . n < +infty )
by A6, A112, A139, A141, EXTREAL1:21, a2;
verum end; end;
end;
hence
(
0. < a . n &
a . n < +infty )
;
verum
end;
hence
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) )
by A126, A56, A52; verum