:: MESFUNC3 semantic presentation
begin
theorem Th1: :: MESFUNC3:1
for n, m being Nat
for a being Function of [:(Seg n),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg n & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
proof
defpred S1[ Nat] means for m being Nat
for a being Function of [:(Seg $1),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg $1 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg $1 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
reconsider n = n as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_for_m_being_Nat
for_a_being_Function_of_[:(Seg_(n_+_1)),(Seg_m):],REAL
for_p,_q_being_FinSequence_of_REAL_st_dom_p_=_Seg_(n_+_1)_&_(_for_i_being_Nat_st_i_in_dom_p_holds_
ex_r_being_FinSequence_of_REAL_st_
(_dom_r_=_Seg_m_&_p_._i_=_Sum_r_&_(_for_j_being_Nat_st_j_in_dom_r_holds_
r_._j_=_a_._[i,j]_)_)_)_&_dom_q_=_Seg_m_&_(_for_j_being_Nat_st_j_in_dom_q_holds_
ex_s_being_FinSequence_of_REAL_st_
(_dom_s_=_Seg_(n_+_1)_&_q_._j_=_Sum_s_&_(_for_i_being_Nat_st_i_in_dom_s_holds_
s_._i_=_a_._[i,j]_)_)_)_holds_
Sum_p_=_Sum_q
let m be Nat; ::_thesis: for a being Function of [:(Seg (n + 1)),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let a be Function of [:(Seg (n + 1)),(Seg m):],REAL; ::_thesis: for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let p, q be FinSequence of REAL ; ::_thesis: ( dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) implies Sum p = Sum q )
assume that
A3: dom p = Seg (n + 1) and
A4: for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) and
A5: dom q = Seg m and
A6: for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ; ::_thesis: Sum p = Sum q
set a0 = a | [:(Seg n),(Seg m):];
n <= n + 1 by NAT_1:11;
then Seg n c= Seg (n + 1) by FINSEQ_1:5;
then [:(Seg n),(Seg m):] c= [:(Seg (n + 1)),(Seg m):] by ZFMISC_1:95;
then reconsider a0 = a | [:(Seg n),(Seg m):] as Function of [:(Seg n),(Seg m):],REAL by FUNCT_2:32;
deffunc H1( Nat) -> Element of REAL = a . [(n + 1),$1];
reconsider p0 = p | (Seg n) as FinSequence of REAL by FINSEQ_1:18;
len p = n + 1 by A3, FINSEQ_1:def_3;
then A7: n <= len p by NAT_1:11;
then A8: dom p0 = Seg n by FINSEQ_1:17;
A9: dom p0 = Seg n by A7, FINSEQ_1:17;
A10: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p0_holds_
ex_r_being_FinSequence_of_REAL_st_
(_dom_r_=_Seg_m_&_p0_._i_=_Sum_r_&_(_for_j_being_Nat_st_j_in_dom_r_holds_
r_._j_=_a0_._[i,j]_)_)
let i be Nat; ::_thesis: ( i in dom p0 implies ex r being FinSequence of REAL st
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) ) )
assume A11: i in dom p0 ; ::_thesis: ex r being FinSequence of REAL st
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) )
consider r being FinSequence of REAL such that
A12: dom r = Seg m and
A13: p . i = Sum r and
A14: for j being Nat st j in dom r holds
r . j = a . [i,j] by A3, A4, A9, A11, FINSEQ_2:8;
take r = r; ::_thesis: ( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) )
thus dom r = Seg m by A12; ::_thesis: ( p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) )
thus p0 . i = Sum r by A11, A13, FUNCT_1:47; ::_thesis: for j being Nat st j in dom r holds
r . j = a0 . [i,j]
thus for j being Nat st j in dom r holds
r . j = a0 . [i,j] ::_thesis: verum
proof
n <= n + 1 by NAT_1:11;
then A15: Seg n c= Seg (n + 1) by FINSEQ_1:5;
dom a = [:(Seg (n + 1)),(Seg m):] by FUNCT_2:def_1;
then A16: dom a0 = [:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):] by RELAT_1:61
.= [:(Seg n),(Seg m):] by A15, ZFMISC_1:101 ;
let j be Nat; ::_thesis: ( j in dom r implies r . j = a0 . [i,j] )
assume A17: j in dom r ; ::_thesis: r . j = a0 . [i,j]
A18: [i,j] in [:(Seg n),(Seg m):] by A9, A11, A12, A17, ZFMISC_1:87;
thus r . j = a . [i,j] by A14, A17
.= a0 . [i,j] by A18, A16, FUNCT_1:47 ; ::_thesis: verum
end;
end;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
consider an being FinSequence such that
A19: ( len an = m & ( for j being Nat st j in dom an holds
an . j = H1(j) ) ) from FINSEQ_1:sch_2();
A20: now__::_thesis:_for_i_being_Nat_st_i_in_dom_an_holds_
an_._i_in_REAL
let i be Nat; ::_thesis: ( i in dom an implies an . i in REAL )
assume i in dom an ; ::_thesis: an . i in REAL
then an . i = a . [(n + 1),i] by A19;
hence an . i in REAL ; ::_thesis: verum
end;
A21: dom an = Seg m by A19, FINSEQ_1:def_3;
reconsider an = an as FinSequence of REAL by A20, FINSEQ_2:12;
A22: an is Element of m -tuples_on REAL by A19, FINSEQ_2:92;
A23: dom an = Seg m by A19, FINSEQ_1:def_3;
A24: Sum an = p . (n + 1)
proof
consider r being FinSequence of REAL such that
A25: dom r = Seg m and
A26: p . (n + 1) = Sum r and
A27: for j being Nat st j in dom r holds
r . j = a . [(n + 1),j] by A3, A4, FINSEQ_1:4;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_r_holds_
r_._j_=_an_._j
let j be Nat; ::_thesis: ( j in dom r implies r . j = an . j )
assume A28: j in dom r ; ::_thesis: r . j = an . j
hence r . j = a . [(n + 1),j] by A27
.= an . j by A19, A21, A25, A28 ;
::_thesis: verum
end;
hence Sum an = p . (n + 1) by A23, A25, A26, FINSEQ_1:13; ::_thesis: verum
end;
reconsider q0 = q - an as FinSequence of REAL ;
A29: rng <:q,an:> c= [:(rng q),(rng an):] by FUNCT_3:51;
dom diffreal = [:REAL,REAL:] by FUNCT_2:def_1;
then A30: [:(rng q),(rng an):] c= dom diffreal by ZFMISC_1:96;
dom (diffreal .: (q,an)) = dom (diffreal * <:q,an:>) by FUNCOP_1:def_3
.= dom <:q,an:> by A30, A29, RELAT_1:27, XBOOLE_1:1
.= (dom q) /\ (dom an) by FUNCT_3:def_7 ;
then A31: dom q0 = (dom q) /\ (dom an) by RVSUM_1:def_6
.= (Seg m) /\ (Seg m) by A5, A19, FINSEQ_1:def_3
.= Seg m ;
then len q0 = m by FINSEQ_1:def_3;
then A32: q0 is Element of m -tuples_on REAL by FINSEQ_2:92;
A33: now__::_thesis:_for_j_being_Nat_st_j_in_dom_q0_holds_
ex_sn_being_FinSequence_of_REAL_st_
(_dom_sn_=_Seg_n_&_q0_._j_=_Sum_sn_&_(_for_i_being_Nat_st_i_in_dom_sn_holds_
sn_._i_=_a0_._[i,j]_)_)
let j be Nat; ::_thesis: ( j in dom q0 implies ex sn being FinSequence of REAL st
( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) ) )
assume A34: j in dom q0 ; ::_thesis: ex sn being FinSequence of REAL st
( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) )
consider s being FinSequence of REAL such that
A35: dom s = Seg (n + 1) and
A36: q . j = Sum s and
A37: for i being Nat st i in dom s holds
s . i = a . [i,j] by A5, A6, A31, A34;
s . (n + 1) = a . [(n + 1),j] by A35, A37, FINSEQ_1:4;
then A38: s . (n + 1) = an . j by A19, A21, A31, A34;
reconsider sn = s | (Seg n) as FinSequence of REAL by FINSEQ_1:18;
take sn = sn; ::_thesis: ( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) )
A39: len s = n + 1 by A35, FINSEQ_1:def_3;
then n <= len s by NAT_1:11;
hence A40: dom sn = Seg n by FINSEQ_1:17; ::_thesis: ( q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) )
sn ^ <*(s . (n + 1))*> = s by A39, FINSEQ_3:55;
then (q . j) - (an . j) = ((Sum sn) + (an . j)) - (an . j) by A36, A38, RVSUM_1:74
.= Sum sn ;
hence q0 . j = Sum sn by A34, VALUED_1:13; ::_thesis: for i being Nat st i in dom sn holds
sn . i = a0 . [i,j]
thus for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ::_thesis: verum
proof
n <= n + 1 by NAT_1:11;
then A41: Seg n c= Seg (n + 1) by FINSEQ_1:5;
dom a = [:(Seg (n + 1)),(Seg m):] by FUNCT_2:def_1;
then A42: dom a0 = [:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):] by RELAT_1:61
.= [:(Seg n),(Seg m):] by A41, ZFMISC_1:101 ;
let i be Nat; ::_thesis: ( i in dom sn implies sn . i = a0 . [i,j] )
assume A43: i in dom sn ; ::_thesis: sn . i = a0 . [i,j]
A44: [i,j] in [:(Seg n),(Seg m):] by A31, A34, A40, A43, ZFMISC_1:87;
thus sn . i = s . i by A43, FUNCT_1:47
.= a . [i,j] by A35, A37, A40, A43, A41
.= a0 . [i,j] by A44, A42, FUNCT_1:47 ; ::_thesis: verum
end;
end;
len q = m by A5, FINSEQ_1:def_3;
then q is Element of m -tuples_on REAL by FINSEQ_2:92;
then A45: q0 + an = q by A22, RVSUM_1:43;
len p = n + 1 by A3, FINSEQ_1:def_3;
then p0 ^ <*(Sum an)*> = p by A24, FINSEQ_3:55;
hence Sum p = (Sum p0) + (Sum an) by RVSUM_1:74
.= (Sum q0) + (Sum an) by A2, A10, A8, A31, A33
.= Sum q by A32, A22, A45, RVSUM_1:89 ;
::_thesis: verum
end;
hence S1[n + 1] ; ::_thesis: verum
end;
now__::_thesis:_for_m_being_Nat
for_a_being_Function_of_[:(Seg_0),(Seg_m):],REAL
for_p,_q_being_FinSequence_of_REAL_st_dom_p_=_Seg_0_&_(_for_i_being_Nat_st_i_in_dom_p_holds_
ex_r_being_FinSequence_of_REAL_st_
(_dom_r_=_Seg_m_&_p_._i_=_Sum_r_&_(_for_j_being_Nat_st_j_in_dom_r_holds_
r_._j_=_a_._[i,j]_)_)_)_&_dom_q_=_Seg_m_&_(_for_j_being_Nat_st_j_in_dom_q_holds_
ex_s_being_FinSequence_of_REAL_st_
(_dom_s_=_Seg_0_&_q_._j_=_Sum_s_&_(_for_i_being_Nat_st_i_in_dom_s_holds_
s_._i_=_a_._[i,j]_)_)_)_holds_
Sum_p_=_Sum_q
let m be Nat; ::_thesis: for a being Function of [:(Seg 0),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let a be Function of [:(Seg 0),(Seg m):],REAL; ::_thesis: for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let p, q be FinSequence of REAL ; ::_thesis: ( dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) implies Sum p = Sum q )
assume that
A46: dom p = Seg 0 and
for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) and
A47: dom q = Seg m and
A48: for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ; ::_thesis: Sum p = Sum q
reconsider m = m as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_for_z_being_set_st_z_in_dom_q_holds_
q_._z_=_0
let z be set ; ::_thesis: ( z in dom q implies q . z = 0 )
assume A49: z in dom q ; ::_thesis: q . z = 0
then z in { k where k is Element of NAT : ( 1 <= k & k <= m ) } by A47, FINSEQ_1:def_1;
then ex k being Element of NAT st
( z = k & 1 <= k & k <= m ) ;
then reconsider j = z as Nat ;
consider s being FinSequence of REAL such that
A50: dom s = Seg 0 and
A51: q . j = Sum s and
for i being Nat st i in dom s holds
s . i = a . [i,j] by A48, A49;
s = <*> REAL by A50;
hence q . z = 0 by A51, RVSUM_1:72; ::_thesis: verum
end;
then q = (dom q) --> 0 by FUNCOP_1:11;
then A52: q = m |-> 0 by A47, FINSEQ_2:def_2;
p = <*> REAL by A46;
hence Sum p = Sum q by A52, RVSUM_1:72, RVSUM_1:81; ::_thesis: verum
end;
then A53: S1[ 0 ] ;
thus for n being Nat holds S1[n] from NAT_1:sch_2(A53, A1); ::_thesis: verum
end;
theorem Th2: :: MESFUNC3:2
for F being FinSequence of ExtREAL
for f being FinSequence of REAL st F = f holds
Sum F = Sum f
proof
let F be FinSequence of ExtREAL ; ::_thesis: for f being FinSequence of REAL st F = f holds
Sum F = Sum f
let f be FinSequence of REAL ; ::_thesis: ( F = f implies Sum F = Sum f )
defpred S1[ Nat] means for G being FinSequence of ExtREAL
for g being FinSequence of REAL st G = F | (Seg $1) & g = f | (Seg $1) & $1 <= len F holds
Sum G = Sum g;
F | (Seg (len F)) = F | (len F) by FINSEQ_1:def_15;
then A1: F | (Seg (len F)) = F by FINSEQ_1:58;
assume A2: F = f ; ::_thesis: Sum F = Sum f
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
for G being FinSequence of ExtREAL
for g being FinSequence of REAL st G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F holds
Sum G = Sum g
proof
let G be FinSequence of ExtREAL ; ::_thesis: for g being FinSequence of REAL st G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F holds
Sum G = Sum g
let g be FinSequence of REAL ; ::_thesis: ( G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F implies Sum G = Sum g )
assume that
A5: G = F | (Seg (k + 1)) and
A6: g = f | (Seg (k + 1)) and
A7: k + 1 <= len F ; ::_thesis: Sum G = Sum g
reconsider g2 = <*(g . (k + 1))*> as FinSequence of REAL ;
reconsider G1 = G | (Seg k) as FinSequence of ExtREAL by FINSEQ_1:18;
A8: now__::_thesis:_(_not_-infty_in_rng_G1_&_not_-infty_in_rng_<*(G_._(k_+_1))*>_)
A9: rng g2 c= REAL ;
assume ( -infty in rng G1 or -infty in rng <*(G . (k + 1))*> ) ; ::_thesis: contradiction
hence contradiction by A2, A5, A6, A9; ::_thesis: verum
end;
reconsider g1 = g | (Seg k) as FinSequence of REAL by FINSEQ_1:18;
len g = k + 1 by A2, A6, A7, FINSEQ_1:17;
then g = g1 ^ <*(g . (k + 1))*> by FINSEQ_3:55;
then A10: Sum g = (Sum g1) + (g . (k + 1)) by RVSUM_1:74;
A11: k <= k + 1 by NAT_1:11;
len G = k + 1 by A5, A7, FINSEQ_1:17;
then G = G1 ^ <*(G . (k + 1))*> by FINSEQ_3:55;
then A12: Sum G = (Sum G1) + (Sum <*(G . (k + 1))*>) by A8, EXTREAL1:10
.= (Sum G1) + (G . (k + 1)) by EXTREAL1:8 ;
k <= k + 1 by NAT_1:11;
then Seg k c= Seg (k + 1) by FINSEQ_1:5;
then ( G1 = F | (Seg k) & g1 = f | (Seg k) ) by A5, A6, FUNCT_1:51;
then Sum G1 = Sum g1 by A4, A7, A11, XXREAL_0:2;
hence Sum G = Sum g by A2, A5, A6, A12, A10, SUPINF_2:1; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A13: S1[ 0 ] by EXTREAL1:7, RVSUM_1:72;
for k being Nat holds S1[k] from NAT_1:sch_2(A13, A3);
hence Sum F = Sum f by A2, A1; ::_thesis: verum
end;
theorem Th3: :: MESFUNC3:3
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & ( for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & ( for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & ( for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
let f be PartFunc of X,ExtREAL; ::_thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & ( for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) )
assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & ( for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
then consider F being Finite_Sep_Sequence of S such that
A1: dom f = union (rng F) and
A2: for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y by MESFUNC2:def_4;
defpred S1[ Nat, Element of ExtREAL ] means for x being set st x in F . $1 holds
$2 = f . x;
A3: for k being Nat st k in Seg (len F) holds
ex y being Element of ExtREAL st S1[k,y]
proof
let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of ExtREAL st S1[k,y] )
assume k in Seg (len F) ; ::_thesis: ex y being Element of ExtREAL st S1[k,y]
then A4: k in dom F by FINSEQ_1:def_3;
then A5: F . k in rng F by FUNCT_1:3;
now__::_thesis:_(_(_F_._k_=_{}_&_ex_y_being_Element_of_ExtREAL_ex_y_being_Element_of_ExtREAL_st_S1[k,y]_)_or_(_F_._k_<>_{}_&_ex_y_being_Element_of_ExtREAL_ex_y_being_Element_of_ExtREAL_st_S1[k,y]_)_)
percases ( F . k = {} or F . k <> {} ) ;
caseA6: F . k = {} ; ::_thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S1[k,y]
take y = 0. ; ::_thesis: ex y being Element of ExtREAL st S1[k,y]
for x being set st x in F . k holds
y = f . x by A6;
hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum
end;
case F . k <> {} ; ::_thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S1[k,y]
then consider x1 being set such that
A7: x1 in F . k by XBOOLE_0:def_1;
take y = f . x1; ::_thesis: ex y being Element of ExtREAL st S1[k,y]
for x being set st x in F . k holds
y = f . x
proof
let x be set ; ::_thesis: ( x in F . k implies y = f . x )
A8: rng F c= bool X by XBOOLE_1:1;
then reconsider x1 = x1 as Element of X by A5, A7;
assume A9: x in F . k ; ::_thesis: y = f . x
then reconsider x = x as Element of X by A5, A8;
f . x = f . x1 by A2, A4, A7, A9;
hence y = f . x ; ::_thesis: verum
end;
hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum
end;
end;
end;
hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum
end;
consider a being FinSequence of ExtREAL such that
A10: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S1[k,a . k] ) ) from FINSEQ_1:sch_5(A3);
take F ; ::_thesis: ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & ( for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
take a ; ::_thesis: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & ( for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
A11: for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) )
proof
let x be set ; ::_thesis: ( x in dom f implies ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) )
assume x in dom f ; ::_thesis: ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) )
deffunc H1( Nat) -> Element of ExtREAL = (a . $1) * ((chi ((F . $1),X)) . x);
consider ax being FinSequence of ExtREAL such that
A12: ( len ax = len F & ( for k being Nat st k in dom ax holds
ax . k = H1(k) ) ) from FINSEQ_2:sch_1();
take ax ; ::_thesis: ( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) )
thus ( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) by A10, A12, FINSEQ_1:def_3; ::_thesis: verum
end;
for n being Nat st n in dom F holds
for x being set st x in F . n holds
a . n = f . x
proof
let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds
a . n = f . x )
assume n in dom F ; ::_thesis: for x being set st x in F . n holds
a . n = f . x
then n in Seg (len F) by FINSEQ_1:def_3;
hence for x being set st x in F . n holds
a . n = f . x by A10; ::_thesis: verum
end;
hence ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & ( for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) by A1, A10, A11, FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th4: :: MESFUNC3:4
for X being set
for F being FinSequence of X holds
( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j )
proof
let X be set ; ::_thesis: for F being FinSequence of X holds
( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j )
let F be FinSequence of X; ::_thesis: ( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j )
now__::_thesis:_(_(_for_i,_j_being_Nat_st_i_in_dom_F_&_j_in_dom_F_&_i_<>_j_holds_
F_._i_misses_F_._j_)_implies_F_is_disjoint_valued_)
assume A1: for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ; ::_thesis: F is disjoint_valued
for x, y being set st x <> y holds
F . x misses F . y
proof
let x, y be set ; ::_thesis: ( x <> y implies F . x misses F . y )
assume A2: x <> y ; ::_thesis: F . x misses F . y
percases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ;
suppose ( x in dom F & y in dom F ) ; ::_thesis: F . x misses F . y
hence F . x misses F . y by A1, A2; ::_thesis: verum
end;
suppose not x in dom F ; ::_thesis: F . x misses F . y
then F . x = {} by FUNCT_1:def_2;
hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum
end;
suppose not y in dom F ; ::_thesis: F . x misses F . y
then F . y = {} by FUNCT_1:def_2;
hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence F is disjoint_valued by PROB_2:def_2; ::_thesis: verum
end;
hence ( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j ) by PROB_2:def_2; ::_thesis: verum
end;
theorem Th5: :: MESFUNC3:5
for X being non empty set
for A being set
for S being SigmaField of X
for F being Finite_Sep_Sequence of S
for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
proof
let X be non empty set ; ::_thesis: for A being set
for S being SigmaField of X
for F being Finite_Sep_Sequence of S
for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
let A be set ; ::_thesis: for S being SigmaField of X
for F being Finite_Sep_Sequence of S
for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
let S be SigmaField of X; ::_thesis: for F being Finite_Sep_Sequence of S
for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
let F be Finite_Sep_Sequence of S; ::_thesis: for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
let G be FinSequence of S; ::_thesis: ( dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) implies G is Finite_Sep_Sequence of S )
assume that
A1: dom G = dom F and
A2: for i being Nat st i in dom G holds
G . i = A /\ (F . i) ; ::_thesis: G is Finite_Sep_Sequence of S
now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_G_&_j_in_dom_G_&_i_<>_j_holds_
G_._i_misses_G_._j
let i, j be Nat; ::_thesis: ( i in dom G & j in dom G & i <> j implies G . i misses G . j )
assume that
A3: i in dom G and
A4: j in dom G and
A5: i <> j ; ::_thesis: G . i misses G . j
A6: F . i misses F . j by A1, A3, A4, A5, Th4;
(A /\ (F . i)) /\ (A /\ (F . j)) = A /\ ((F . i) /\ (A /\ (F . j))) by XBOOLE_1:16
.= A /\ (((F . i) /\ (F . j)) /\ A) by XBOOLE_1:16
.= A /\ ({} /\ A) by A6, XBOOLE_0:def_7
.= {} ;
then A /\ (F . i) misses A /\ (F . j) by XBOOLE_0:def_7;
then G . i misses A /\ (F . j) by A2, A3;
hence G . i misses G . j by A2, A4; ::_thesis: verum
end;
hence G is Finite_Sep_Sequence of S by Th4; ::_thesis: verum
end;
theorem Th6: :: MESFUNC3:6
for X being non empty set
for A being set
for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
union (rng G) = A /\ (union (rng F))
proof
let X be non empty set ; ::_thesis: for A being set
for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
union (rng G) = A /\ (union (rng F))
let A be set ; ::_thesis: for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
union (rng G) = A /\ (union (rng F))
let F, G be FinSequence of X; ::_thesis: ( dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) implies union (rng G) = A /\ (union (rng F)) )
assume that
A1: dom G = dom F and
A2: for i being Nat st i in dom G holds
G . i = A /\ (F . i) ; ::_thesis: union (rng G) = A /\ (union (rng F))
thus union (rng G) c= A /\ (union (rng F)) :: according to XBOOLE_0:def_10 ::_thesis: A /\ (union (rng F)) c= union (rng G)
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng G) or r in A /\ (union (rng F)) )
assume r in union (rng G) ; ::_thesis: r in A /\ (union (rng F))
then consider E being set such that
A3: r in E and
A4: E in rng G by TARSKI:def_4;
consider s being set such that
A5: s in dom G and
A6: E = G . s by A4, FUNCT_1:def_3;
reconsider s = s as Element of NAT by A5;
A7: r in A /\ (F . s) by A2, A3, A5, A6;
then A8: r in F . s by XBOOLE_0:def_4;
F . s in rng F by A1, A5, FUNCT_1:3;
then A9: r in union (rng F) by A8, TARSKI:def_4;
r in A by A7, XBOOLE_0:def_4;
hence r in A /\ (union (rng F)) by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in A /\ (union (rng F)) or r in union (rng G) )
assume A10: r in A /\ (union (rng F)) ; ::_thesis: r in union (rng G)
then A11: r in A by XBOOLE_0:def_4;
r in union (rng F) by A10, XBOOLE_0:def_4;
then consider E being set such that
A12: r in E and
A13: E in rng F by TARSKI:def_4;
consider s being set such that
A14: s in dom F and
A15: E = F . s by A13, FUNCT_1:def_3;
reconsider s = s as Element of NAT by A14;
A /\ E = G . s by A1, A2, A14, A15;
then A16: r in G . s by A11, A12, XBOOLE_0:def_4;
G . s in rng G by A1, A14, FUNCT_1:3;
hence r in union (rng G) by A16, TARSKI:def_4; ::_thesis: verum
end;
theorem Th7: :: MESFUNC3:7
for X being set
for F being FinSequence of X
for i being Nat st i in dom F holds
( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )
proof
let X be set ; ::_thesis: for F being FinSequence of X
for i being Nat st i in dom F holds
( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )
let F be FinSequence of X; ::_thesis: for i being Nat st i in dom F holds
( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )
let i be Nat; ::_thesis: ( i in dom F implies ( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i ) )
assume A1: i in dom F ; ::_thesis: ( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )
hence F . i c= union (rng F) by FUNCT_1:3, ZFMISC_1:74; ::_thesis: (F . i) /\ (union (rng F)) = F . i
F . i in rng F by A1, FUNCT_1:3;
hence (F . i) /\ (union (rng F)) = F . i by XBOOLE_1:28, ZFMISC_1:74; ::_thesis: verum
end;
theorem Th8: :: MESFUNC3:8
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds dom F = dom (M * F)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds dom F = dom (M * F)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds dom F = dom (M * F)
let M be sigma_Measure of S; ::_thesis: for F being Finite_Sep_Sequence of S holds dom F = dom (M * F)
let F be Finite_Sep_Sequence of S; ::_thesis: dom F = dom (M * F)
dom M = S by FUNCT_2:def_1;
then rng F c= dom M ;
hence dom F = dom (M * F) by RELAT_1:27; ::_thesis: verum
end;
theorem Th9: :: MESFUNC3:9
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)
let M be sigma_Measure of S; ::_thesis: for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)
let F be Finite_Sep_Sequence of S; ::_thesis: M . (union (rng F)) = Sum (M * F)
reconsider F1 = M * F as FinSequence of ExtREAL ;
consider f being Function of NAT,ExtREAL such that
A1: Sum F1 = f . (len F1) and
A2: f . 0 = 0. and
A3: for i being Element of NAT st i < len F1 holds
f . (i + 1) = (f . i) + (F1 . (i + 1)) by EXTREAL1:def_2;
consider G being Sep_Sequence of S such that
A4: union (rng F) = union (rng G) and
A5: for n being Nat st n in dom F holds
F . n = G . n and
A6: for m being Nat st not m in dom F holds
G . m = {} by MESFUNC2:30;
defpred S1[ Nat] means ( $1 <= len F1 implies (Ser (M * G)) . $1 = f . $1 );
reconsider G1 = M * G as Num of rng (M * G) by SUPINF_2:def_10;
A7: dom G = NAT by FUNCT_2:def_1;
A8: Ser (M * G) = Ser ((rng (M * G)),G1) by SUPINF_2:def_15;
A9: for i being Nat st i < len F1 holds
(Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1))
proof
let i be Nat; ::_thesis: ( i < len F1 implies (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1)) )
assume i < len F1 ; ::_thesis: (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1))
then ( 1 <= i + 1 & i + 1 <= len F1 ) by NAT_1:11, NAT_1:13;
then i + 1 in dom F1 by FINSEQ_3:25;
then A10: i + 1 in dom F by Th8;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
(Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (G1 . (i + 1)) by A8, SUPINF_2:def_11
.= ((Ser (M * G)) . i) + (M . (G . (i + 1))) by A7, FUNCT_1:13
.= ((Ser (M * G)) . i) + (M . (F . (i + 1))) by A5, A10 ;
hence (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1)) by A10, FUNCT_1:13; ::_thesis: verum
end;
A11: for k being Nat st S1[k] holds
S1[k + 1]
proof
A12: for i being Nat st i < len F1 holds
f . (i + 1) = (f . i) + (F1 . (i + 1))
proof
let i be Nat; ::_thesis: ( i < len F1 implies f . (i + 1) = (f . i) + (F1 . (i + 1)) )
i in NAT by ORDINAL1:def_12;
hence ( i < len F1 implies f . (i + 1) = (f . i) + (F1 . (i + 1)) ) by A3; ::_thesis: verum
end;
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A13: S1[k] ; ::_thesis: S1[k + 1]
assume k + 1 <= len F1 ; ::_thesis: (Ser (M * G)) . (k + 1) = f . (k + 1)
then A14: k < len F1 by NAT_1:13;
then (Ser (M * G)) . (k + 1) = (f . k) + (F1 . (k + 1)) by A9, A13;
hence (Ser (M * G)) . (k + 1) = f . (k + 1) by A12, A14; ::_thesis: verum
end;
defpred S2[ Nat] means ( $1 >= len F1 implies (Ser (M * G)) . $1 = (Ser (M * G)) . (len F1) );
A15: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A16: S2[k] ; ::_thesis: S2[k + 1]
assume A17: k + 1 >= len F1 ; ::_thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1)
reconsider k = k as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_(_(_k_>=_len_F1_&_(Ser_(M_*_G))_._(k_+_1)_=_(Ser_(M_*_G))_._(len_F1)_)_or_(_k_<_len_F1_&_(Ser_(M_*_G))_._(k_+_1)_=_(Ser_(M_*_G))_._(len_F1)_)_)
percases ( k >= len F1 or k < len F1 ) ;
caseA18: k >= len F1 ; ::_thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1)
then k + 1 > len F1 by NAT_1:13;
then not k + 1 in Seg (len F1) by FINSEQ_1:1;
then not k + 1 in dom F1 by FINSEQ_1:def_3;
then A19: not k + 1 in dom F by Th8;
A20: G1 . (k + 1) = M . (G . (k + 1)) by A7, FUNCT_1:13
.= M . {} by A6, A19
.= 0. by VALUED_0:def_19 ;
(Ser (M * G)) . (k + 1) = ((Ser (M * G)) . (len F1)) + (G1 . (k + 1)) by A8, A16, A18, SUPINF_2:def_11;
hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) by A20, XXREAL_3:4; ::_thesis: verum
end;
case k < len F1 ; ::_thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1)
then k + 1 <= len F1 by NAT_1:13;
hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) by A17, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) ; ::_thesis: verum
end;
defpred S3[ Nat] means ( $1 < len F1 implies (Ser (M * G)) . ((len F1) - $1) <= (Ser (M * G)) . (len F1) );
A21: M * G is V103() by MEASURE2:1;
A22: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; ::_thesis: ( S3[k] implies S3[k + 1] )
assume A23: S3[k] ; ::_thesis: S3[k + 1]
assume A24: k + 1 < len F1 ; ::_thesis: (Ser (M * G)) . ((len F1) - (k + 1)) <= (Ser (M * G)) . (len F1)
then consider k9 being Nat such that
A25: len F1 = (k + 1) + k9 by NAT_1:10;
reconsider k9 = k9 as Element of NAT by ORDINAL1:def_12;
( k <= k + 1 & (Ser (M * G)) . k9 <= (Ser (M * G)) . (k9 + 1) ) by A21, NAT_1:11, SUPINF_2:40;
hence (Ser (M * G)) . ((len F1) - (k + 1)) <= (Ser (M * G)) . (len F1) by A23, A24, A25, XXREAL_0:2; ::_thesis: verum
end;
not 0 in Seg (len F) by FINSEQ_1:1;
then not 0 in dom F by FINSEQ_1:def_3;
then A26: G . 0 = {} by A6;
(Ser (M * G)) . 0 = G1 . 0 by A8, SUPINF_2:def_11;
then A27: (Ser (M * G)) . 0 = M . (G . 0) by A7, FUNCT_1:13
.= 0. by A26, VALUED_0:def_19 ;
then A28: S1[ 0 ] by A2;
A29: for k being Nat holds S1[k] from NAT_1:sch_2(A28, A11);
A30: S3[ 0 ] ;
A31: for i being Nat holds S3[i] from NAT_1:sch_2(A30, A22);
A32: for i being Nat st i < len F1 holds
(Ser (M * G)) . i <= (Ser (M * G)) . (len F1)
proof
let i be Nat; ::_thesis: ( i < len F1 implies (Ser (M * G)) . i <= (Ser (M * G)) . (len F1) )
A33: len F1 <= (len F1) + i by NAT_1:11;
assume i < len F1 ; ::_thesis: (Ser (M * G)) . i <= (Ser (M * G)) . (len F1)
then consider k being Nat such that
A34: len F1 = i + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
k = (len F1) - i by A34;
then A35: k <= len F1 by A33, XREAL_1:20;
(Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1)
proof
now__::_thesis:_(_(_k_=_len_F1_&_(Ser_(M_*_G))_._((len_F1)_-_k)_<=_(Ser_(M_*_G))_._(len_F1)_)_or_(_k_<_len_F1_&_(Ser_(M_*_G))_._((len_F1)_-_k)_<=_(Ser_(M_*_G))_._(len_F1)_)_)
percases ( k = len F1 or k < len F1 ) by A35, XXREAL_0:1;
case k = len F1 ; ::_thesis: (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1)
hence (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) by A27, A21, SUPINF_2:40; ::_thesis: verum
end;
case k < len F1 ; ::_thesis: (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1)
hence (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) by A31; ::_thesis: verum
end;
end;
end;
hence (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) ; ::_thesis: verum
end;
hence (Ser (M * G)) . i <= (Ser (M * G)) . (len F1) by A34; ::_thesis: verum
end;
A36: S2[ 0 ] ;
A37: for k being Nat holds S2[k] from NAT_1:sch_2(A36, A15);
for z being ext-real number st z in rng (Ser (M * G)) holds
z <= (Ser (M * G)) . (len F1)
proof
let z be ext-real number ; ::_thesis: ( z in rng (Ser (M * G)) implies z <= (Ser (M * G)) . (len F1) )
assume z in rng (Ser (M * G)) ; ::_thesis: z <= (Ser (M * G)) . (len F1)
then consider n being set such that
A38: n in dom (Ser (M * G)) and
A39: z = (Ser (M * G)) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A38;
now__::_thesis:_(_(_n_<_len_F1_&_z_<=_(Ser_(M_*_G))_._(len_F1)_)_or_(_n_>=_len_F1_&_z_<=_(Ser_(M_*_G))_._(len_F1)_)_)
percases ( n < len F1 or n >= len F1 ) ;
case n < len F1 ; ::_thesis: z <= (Ser (M * G)) . (len F1)
hence z <= (Ser (M * G)) . (len F1) by A32, A39; ::_thesis: verum
end;
case n >= len F1 ; ::_thesis: z <= (Ser (M * G)) . (len F1)
hence z <= (Ser (M * G)) . (len F1) by A37, A39; ::_thesis: verum
end;
end;
end;
hence z <= (Ser (M * G)) . (len F1) ; ::_thesis: verum
end;
then A40: (Ser (M * G)) . (len F1) is UpperBound of rng (Ser (M * G)) by XXREAL_2:def_1;
dom (Ser (M * G)) = NAT by FUNCT_2:def_1;
then A41: (Ser (M * G)) . (len F1) = sup (rng (Ser (M * G))) by A40, FUNCT_1:3, XXREAL_2:55;
M . (union (rng F)) = SUM (M * G) by A4, MEASURE1:def_6
.= sup (rng (Ser (M * G))) ;
hence M . (union (rng F)) = Sum (M * F) by A1, A29, A41; ::_thesis: verum
end;
theorem Th10: :: MESFUNC3:10
for F, G being FinSequence of ExtREAL
for a being R_eal st ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds
G . i = a * (F . i) ) holds
Sum G = a * (Sum F)
proof
let F, G be FinSequence of ExtREAL ; ::_thesis: for a being R_eal st ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds
G . i = a * (F . i) ) holds
Sum G = a * (Sum F)
let a be R_eal; ::_thesis: ( ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds
G . i = a * (F . i) ) implies Sum G = a * (Sum F) )
assume that
A1: ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) and
A2: dom F = dom G and
A3: for i being Nat st i in dom G holds
G . i = a * (F . i) ; ::_thesis: Sum G = a * (Sum F)
consider g being Function of NAT,ExtREAL such that
A4: Sum G = g . (len G) and
A5: g . 0 = 0. and
A6: for i being Element of NAT st i < len G holds
g . (i + 1) = (g . i) + (G . (i + 1)) by EXTREAL1:def_2;
consider f being Function of NAT,ExtREAL such that
A7: Sum F = f . (len F) and
A8: f . 0 = 0. and
A9: for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) by EXTREAL1:def_2;
defpred S1[ Nat] means ( $1 <= len G implies g . $1 = a * (f . $1) );
A10: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A11: S1[i] ; ::_thesis: S1[i + 1]
assume A12: i + 1 <= len G ; ::_thesis: g . (i + 1) = a * (f . (i + 1))
reconsider i = i as Element of NAT by ORDINAL1:def_12;
1 <= i + 1 by NAT_1:11;
then A13: i + 1 in dom G by A12, FINSEQ_3:25;
then i + 1 in Seg (len F) by A2, FINSEQ_1:def_3;
then i + 1 <= len F by FINSEQ_1:1;
then A14: i < len F by NAT_1:13;
i < len G by A12, NAT_1:13;
then A15: g . (i + 1) = (g . i) + (G . (i + 1)) by A6
.= (a * (f . i)) + (a * (F . (i + 1))) by A3, A11, A12, A13, NAT_1:13 ;
now__::_thesis:_(_(_a_is_real_&_g_._(i_+_1)_=_a_*_(f_._(i_+_1))_)_or_(_(_for_i_being_Nat_st_i_in_dom_F_holds_
F_._i_<_0._)_&_g_._(i_+_1)_=_a_*_(f_._(i_+_1))_)_or_(_(_for_i_being_Nat_st_i_in_dom_F_holds_
0._<_F_._i_)_&_g_._(i_+_1)_=_a_*_(f_._(i_+_1))_)_)
percases ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) by A1;
case a is real ; ::_thesis: g . (i + 1) = a * (f . (i + 1))
then g . (i + 1) = a * ((f . i) + (F . (i + 1))) by A15, XXREAL_3:95;
hence g . (i + 1) = a * (f . (i + 1)) by A9, A14; ::_thesis: verum
end;
caseA16: for i being Nat st i in dom F holds
F . i < 0. ; ::_thesis: g . (i + 1) = a * (f . (i + 1))
defpred S2[ Nat] means ( $1 < len F implies f . $1 <= 0. );
A17: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] )
assume A18: S2[i] ; ::_thesis: S2[i + 1]
assume A19: i + 1 < len F ; ::_thesis: f . (i + 1) <= 0.
reconsider i = i as Element of NAT by ORDINAL1:def_12;
1 <= i + 1 by NAT_1:12;
then i + 1 in dom F by A19, FINSEQ_3:25;
then A20: F . (i + 1) < 0. by A16;
i < len F by A19, NAT_1:13;
then f . (i + 1) = (f . i) + (F . (i + 1)) by A9;
hence f . (i + 1) <= 0. by A18, A19, A20, NAT_1:13; ::_thesis: verum
end;
A21: S2[ 0 ] by A8;
for i being Nat holds S2[i] from NAT_1:sch_2(A21, A17);
then A22: ( f . i < 0. or f . i = 0. ) by A14;
F . (i + 1) < 0. by A2, A13, A16;
then g . (i + 1) = a * ((f . i) + (F . (i + 1))) by A15, A22, XXREAL_3:97;
hence g . (i + 1) = a * (f . (i + 1)) by A9, A14; ::_thesis: verum
end;
caseA23: for i being Nat st i in dom F holds
0. < F . i ; ::_thesis: g . (i + 1) = a * (f . (i + 1))
defpred S2[ Nat] means ( $1 < len F implies 0. <= f . $1 );
A24: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] )
assume A25: S2[i] ; ::_thesis: S2[i + 1]
assume A26: i + 1 < len F ; ::_thesis: 0. <= f . (i + 1)
reconsider i = i as Element of NAT by ORDINAL1:def_12;
1 <= i + 1 by NAT_1:12;
then i + 1 in dom F by A26, FINSEQ_3:25;
then A27: 0. < F . (i + 1) by A23;
i < len F by A26, NAT_1:13;
then f . (i + 1) = (f . i) + (F . (i + 1)) by A9;
hence 0. <= f . (i + 1) by A25, A26, A27, NAT_1:13; ::_thesis: verum
end;
A28: S2[ 0 ] by A8;
for i being Nat holds S2[i] from NAT_1:sch_2(A28, A24);
then A29: ( 0. < f . i or f . i = 0. ) by A14;
0. < F . (i + 1) by A2, A13, A23;
then g . (i + 1) = a * ((f . i) + (F . (i + 1))) by A15, A29, XXREAL_3:96;
hence g . (i + 1) = a * (f . (i + 1)) by A9, A14; ::_thesis: verum
end;
end;
end;
hence g . (i + 1) = a * (f . (i + 1)) ; ::_thesis: verum
end;
A30: S1[ 0 ] by A8, A5;
A31: for i being Nat holds S1[i] from NAT_1:sch_2(A30, A10);
Seg (len F) = dom G by A2, FINSEQ_1:def_3
.= Seg (len G) by FINSEQ_1:def_3 ;
then a * (Sum F) = a * (f . (len G)) by A7, FINSEQ_1:6
.= g . (len G) by A31 ;
hence Sum G = a * (Sum F) by A4; ::_thesis: verum
end;
theorem Th11: :: MESFUNC3:11
for F being FinSequence of REAL holds F is FinSequence of ExtREAL
proof
let F be FinSequence of REAL ; ::_thesis: F is FinSequence of ExtREAL
rng F c= ExtREAL by NUMBERS:31, XBOOLE_1:1;
hence F is FinSequence of ExtREAL by FINSEQ_1:def_4; ::_thesis: verum
end;
definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
let F be Finite_Sep_Sequence of S;
let a be FinSequence of ExtREAL ;
predF,a are_Re-presentation_of f means :Def1: :: MESFUNC3:def 1
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) );
end;
:: deftheorem Def1 defines are_Re-presentation_of MESFUNC3:def_1_:_
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL holds
( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) );
theorem :: MESFUNC3:12
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f
let f be PartFunc of X,ExtREAL; ::_thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f )
assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f
then consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A1: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) and
for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) by Th3;
take F ; ::_thesis: ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f
take a ; ::_thesis: F,a are_Re-presentation_of f
thus F,a are_Re-presentation_of f by A1, Def1; ::_thesis: verum
end;
theorem Th13: :: MESFUNC3:13
for X being non empty set
for S being SigmaField of X
for F being Finite_Sep_Sequence of S ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for F being Finite_Sep_Sequence of S ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) )
let S be SigmaField of X; ::_thesis: for F being Finite_Sep_Sequence of S ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) )
let F be Finite_Sep_Sequence of S; ::_thesis: ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) )
defpred S1[ Nat] means for F being Finite_Sep_Sequence of S st len F = $1 holds
ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let F be Finite_Sep_Sequence of S; ::_thesis: ( len F = n + 1 implies ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) ) )
assume A3: len F = n + 1 ; ::_thesis: ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) )
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider F1 = F | (Seg n) as Finite_Sep_Sequence of S by MESFUNC2:33;
A4: n <= len F by A3, NAT_1:11;
then A5: len F1 = n by FINSEQ_1:17;
then consider G1 being Finite_Sep_Sequence of S such that
A6: union (rng F1) = union (rng G1) and
A7: for n being Nat st n in dom G1 holds
( G1 . n <> {} & ex m being Nat st
( m in dom F1 & F1 . m = G1 . n ) ) by A2;
A8: ( dom F = dom (F1 ^ <*(F . (n + 1))*>) & ( for k being Nat st k in dom F holds
F . k = (F1 ^ <*(F . (n + 1))*>) . k ) )
proof
thus dom (F1 ^ <*(F . (n + 1))*>) = Seg ((len F1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:def_7
.= Seg (n + 1) by A5, FINSEQ_1:39
.= dom F by A3, FINSEQ_1:def_3 ; ::_thesis: for k being Nat st k in dom F holds
F . k = (F1 ^ <*(F . (n + 1))*>) . k
let k be Nat; ::_thesis: ( k in dom F implies F . k = (F1 ^ <*(F . (n + 1))*>) . k )
assume A9: k in dom F ; ::_thesis: F . k = (F1 ^ <*(F . (n + 1))*>) . k
now__::_thesis:_(_(_k_in_dom_F1_&_F_._k_=_(F1_^_<*(F_._(n_+_1))*>)_._k_)_or_(_not_k_in_dom_F1_&_F_._k_=_(F1_^_<*(F_._(n_+_1))*>)_._k_)_)
percases ( k in dom F1 or not k in dom F1 ) ;
caseA10: k in dom F1 ; ::_thesis: F . k = (F1 ^ <*(F . (n + 1))*>) . k
then k in Seg n by A4, FINSEQ_1:17;
then k <= n by FINSEQ_1:1;
then A11: (F | n) . k = F . k by FINSEQ_3:112;
(F1 ^ <*(F . (n + 1))*>) . k = F1 . k by A10, FINSEQ_1:def_7;
hence F . k = (F1 ^ <*(F . (n + 1))*>) . k by A11, FINSEQ_1:def_15; ::_thesis: verum
end;
caseA12: not k in dom F1 ; ::_thesis: F . k = (F1 ^ <*(F . (n + 1))*>) . k
A13: k in Seg (n + 1) by A3, A9, FINSEQ_1:def_3;
not k in Seg n by A4, A12, FINSEQ_1:17;
then ( not 1 <= k or not k <= n ) by FINSEQ_1:1;
then A14: not k < n + 1 by A13, FINSEQ_1:1, NAT_1:13;
dom <*(F . (n + 1))*> = Seg 1 by FINSEQ_1:def_8;
then A15: 1 in dom <*(F . (n + 1))*> by FINSEQ_1:2, TARSKI:def_1;
A16: k <= n + 1 by A13, FINSEQ_1:1;
then (F1 ^ <*(F . (n + 1))*>) . k = (F1 ^ <*(F . (n + 1))*>) . ((len F1) + 1) by A5, A14, XXREAL_0:1
.= <*(F . (n + 1))*> . 1 by A15, FINSEQ_1:def_7
.= F . (n + 1) by FINSEQ_1:def_8 ;
hence F . k = (F1 ^ <*(F . (n + 1))*>) . k by A14, A16, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence F . k = (F1 ^ <*(F . (n + 1))*>) . k ; ::_thesis: verum
end;
then A17: F = F1 ^ <*(F . (n + 1))*> by FINSEQ_1:13;
ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) )
proof
now__::_thesis:_(_(_F_._(n_+_1)_=_{}_&_ex_G,_G_being_Finite_Sep_Sequence_of_S_st_
(_union_(rng_F)_=_union_(rng_G)_&_(_for_k_being_Nat_st_k_in_dom_G_holds_
(_G_._k_<>_{}_&_ex_m_being_Nat_st_
(_m_in_dom_F_&_F_._m_=_G_._k_)_)_)_)_)_or_(_F_._(n_+_1)_<>_{}_&_ex_G,_G_being_Finite_Sep_Sequence_of_S_st_
(_union_(rng_F)_=_union_(rng_G)_&_(_for_k_being_Nat_st_k_in_dom_G_holds_
(_G_._k_<>_{}_&_ex_m_being_Nat_st_
(_m_in_dom_F_&_F_._m_=_G_._k_)_)_)_)_)_)
percases ( F . (n + 1) = {} or F . (n + 1) <> {} ) ;
case F . (n + 1) = {} ; ::_thesis: ex G, G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) )
then A18: rng <*(F . (n + 1))*> = {{}} by FINSEQ_1:38;
take G = G1; ::_thesis: ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) )
A19: for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) )
proof
let k be Nat; ::_thesis: ( k in dom G implies ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) )
A20: dom F1 c= dom F by A8, FINSEQ_1:26;
assume A21: k in dom G ; ::_thesis: ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) )
then consider m being Nat such that
A22: m in dom F1 and
A23: F1 . m = G . k by A7;
F1 . m = F . m by A17, A22, FINSEQ_1:def_7;
hence ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) by A7, A21, A22, A23, A20; ::_thesis: verum
end;
rng F = (rng F1) \/ (rng <*(F . (n + 1))*>) by A17, FINSEQ_1:31;
then union (rng F) = (union (rng F1)) \/ (union (rng <*(F . (n + 1))*>)) by ZFMISC_1:78
.= (union (rng F1)) \/ {} by A18, ZFMISC_1:25
.= union (rng G) by A6 ;
hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) ) by A19; ::_thesis: verum
end;
caseA24: F . (n + 1) <> {} ; ::_thesis: ex G, G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) )
A25: for k, m being set st k <> m holds
(G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m
proof
let k, m be set ; ::_thesis: ( k <> m implies (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m )
assume A26: k <> m ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m
now__::_thesis:_(_(_k_in_dom_(G1_^_<*(F_._(n_+_1))*>)_&_m_in_dom_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_or_(_(_not_k_in_dom_(G1_^_<*(F_._(n_+_1))*>)_or_not_m_in_dom_(G1_^_<*(F_._(n_+_1))*>)_)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_)
percases ( ( k in dom (G1 ^ <*(F . (n + 1))*>) & m in dom (G1 ^ <*(F . (n + 1))*>) ) or not k in dom (G1 ^ <*(F . (n + 1))*>) or not m in dom (G1 ^ <*(F . (n + 1))*>) ) ;
caseA27: ( k in dom (G1 ^ <*(F . (n + 1))*>) & m in dom (G1 ^ <*(F . (n + 1))*>) ) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m
then reconsider k = k, m = m as Element of NAT ;
now__::_thesis:_(_(_k_=_len_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_or_(_k_<>_len_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_)
percases ( k = len (G1 ^ <*(F . (n + 1))*>) or k <> len (G1 ^ <*(F . (n + 1))*>) ) ;
case k = len (G1 ^ <*(F . (n + 1))*>) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m
then k = (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22;
then A28: k = (len G1) + 1 by FINSEQ_1:39;
1 <= len <*(F . (n + 1))*> by FINSEQ_1:39;
then A29: (G1 ^ <*(F . (n + 1))*>) . k = <*(F . (n + 1))*> . 1 by A28, FINSEQ_1:65
.= F . (n + 1) by FINSEQ_1:def_8 ;
A30: m in Seg (len (G1 ^ <*(F . (n + 1))*>)) by A27, FINSEQ_1:def_3;
then m in Seg ((len G1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:22;
then m in Seg ((len G1) + 1) by FINSEQ_1:39;
then m <= (len G1) + 1 by FINSEQ_1:1;
then m < (len G1) + 1 by A26, A28, XXREAL_0:1;
then A31: m <= len G1 by NAT_1:13;
1 <= m by A30, FINSEQ_1:1;
then A32: m in dom G1 by A31, FINSEQ_3:25;
then consider m1 being Nat such that
A33: m1 in dom F1 and
A34: F1 . m1 = G1 . m by A7;
m1 in Seg (len F1) by A33, FINSEQ_1:def_3;
then m1 <= n by A5, FINSEQ_1:1;
then A35: m1 <> n + 1 by NAT_1:13;
(G1 ^ <*(F . (n + 1))*>) . m = G1 . m by A32, FINSEQ_1:def_7;
then (G1 ^ <*(F . (n + 1))*>) . m = F . m1 by A17, A33, A34, FINSEQ_1:def_7;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by A29, A35, PROB_2:def_2; ::_thesis: verum
end;
case k <> len (G1 ^ <*(F . (n + 1))*>) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m
then k <> (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22;
then A36: k <> (len G1) + 1 by FINSEQ_1:39;
A37: k in Seg (len (G1 ^ <*(F . (n + 1))*>)) by A27, FINSEQ_1:def_3;
then k in Seg ((len G1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:22;
then k in Seg ((len G1) + 1) by FINSEQ_1:39;
then k <= (len G1) + 1 by FINSEQ_1:1;
then k < (len G1) + 1 by A36, XXREAL_0:1;
then A38: k <= len G1 by NAT_1:13;
1 <= k by A37, FINSEQ_1:1;
then A39: k in dom G1 by A38, FINSEQ_3:25;
then A40: (G1 ^ <*(F . (n + 1))*>) . k = G1 . k by FINSEQ_1:def_7;
now__::_thesis:_(_(_m_=_len_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_or_(_m_<>_len_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_)
percases ( m = len (G1 ^ <*(F . (n + 1))*>) or m <> len (G1 ^ <*(F . (n + 1))*>) ) ;
case m = len (G1 ^ <*(F . (n + 1))*>) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m
then m = (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22;
then A41: m = (len G1) + 1 by FINSEQ_1:39;
1 <= len <*(F . (n + 1))*> by FINSEQ_1:39;
then A42: (G1 ^ <*(F . (n + 1))*>) . m = <*(F . (n + 1))*> . 1 by A41, FINSEQ_1:65
.= F . (n + 1) by FINSEQ_1:def_8 ;
consider k1 being Nat such that
A43: k1 in dom F1 and
A44: F1 . k1 = G1 . k by A7, A39;
k1 in Seg (len F1) by A43, FINSEQ_1:def_3;
then k1 <= n by A5, FINSEQ_1:1;
then A45: k1 <> n + 1 by NAT_1:13;
(G1 ^ <*(F . (n + 1))*>) . k = F . k1 by A17, A40, A43, A44, FINSEQ_1:def_7;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by A42, A45, PROB_2:def_2; ::_thesis: verum
end;
case m <> len (G1 ^ <*(F . (n + 1))*>) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m
then m <> (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22;
then A46: m <> (len G1) + 1 by FINSEQ_1:39;
A47: m in Seg (len (G1 ^ <*(F . (n + 1))*>)) by A27, FINSEQ_1:def_3;
then m in Seg ((len G1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:22;
then m in Seg ((len G1) + 1) by FINSEQ_1:39;
then m <= (len G1) + 1 by FINSEQ_1:1;
then m < (len G1) + 1 by A46, XXREAL_0:1;
then A48: m <= len G1 by NAT_1:13;
1 <= m by A47, FINSEQ_1:1;
then m in dom G1 by A48, FINSEQ_3:25;
then (G1 ^ <*(F . (n + 1))*>) . m = G1 . m by FINSEQ_1:def_7;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by A26, A40, PROB_2:def_2; ::_thesis: verum
end;
end;
end;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; ::_thesis: verum
end;
end;
end;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; ::_thesis: verum
end;
case ( not k in dom (G1 ^ <*(F . (n + 1))*>) or not m in dom (G1 ^ <*(F . (n + 1))*>) ) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m
then ( (G1 ^ <*(F . (n + 1))*>) . k = {} or (G1 ^ <*(F . (n + 1))*>) . m = {} ) by FUNCT_1:def_2;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; ::_thesis: verum
end;
1 <= n + 1 by NAT_1:11;
then n + 1 in Seg (n + 1) by FINSEQ_1:1;
then n + 1 in dom F by A3, FINSEQ_1:def_3;
then F . (n + 1) in rng F by FUNCT_1:3;
then <*(F . (n + 1))*> is FinSequence of S by FINSEQ_1:74;
then reconsider G = G1 ^ <*(F . (n + 1))*> as Finite_Sep_Sequence of S by A25, FINSEQ_1:75, PROB_2:def_2;
A49: len G = (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22
.= (len G1) + 1 by FINSEQ_1:39 ;
A50: for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) )
proof
let k be Nat; ::_thesis: ( k in dom G implies ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) )
assume A51: k in dom G ; ::_thesis: ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) )
reconsider k = k as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_(_(_k_=_len_G_&_G_._k_<>_{}_&_ex_m_being_Nat_st_
(_m_in_dom_F_&_F_._m_=_G_._k_)_)_or_(_k_<>_len_G_&_G_._k_<>_{}_&_ex_m_being_Nat_st_
(_m_in_dom_F_&_F_._m_=_G_._k_)_)_)
percases ( k = len G or k <> len G ) ;
caseA52: k = len G ; ::_thesis: ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) )
1 <= n + 1 by NAT_1:11;
then n + 1 in Seg (n + 1) by FINSEQ_1:1;
then A53: n + 1 in dom F by A3, FINSEQ_1:def_3;
dom <*(F . (n + 1))*> = Seg 1 by FINSEQ_1:38;
then 1 in dom <*(F . (n + 1))*> by FINSEQ_1:2, TARSKI:def_1;
then G . k = <*(F . (n + 1))*> . 1 by A49, A52, FINSEQ_1:def_7
.= F . (n + 1) by FINSEQ_1:def_8 ;
hence ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) by A24, A53; ::_thesis: verum
end;
caseA54: k <> len G ; ::_thesis: ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) )
k <= len G by A51, FINSEQ_3:25;
then k < len G by A54, XXREAL_0:1;
then A55: k <= len G1 by A49, NAT_1:13;
1 <= k by A51, FINSEQ_3:25;
then A56: k in dom G1 by A55, FINSEQ_3:25;
then A57: G . k = G1 . k by FINSEQ_1:def_7;
ex m being Nat st
( m in dom F & F . m = G . k )
proof
consider m being Nat such that
A58: ( m in dom F1 & F1 . m = G1 . k ) by A7, A56;
take m ; ::_thesis: ( m in dom F & F . m = G . k )
dom F1 c= dom F by A8, FINSEQ_1:26;
hence ( m in dom F & F . m = G . k ) by A17, A57, A58, FINSEQ_1:def_7; ::_thesis: verum
end;
hence ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) by A7, A56, A57; ::_thesis: verum
end;
end;
end;
hence ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ; ::_thesis: verum
end;
take G = G; ::_thesis: ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) )
rng F = (rng F1) \/ (rng <*(F . (n + 1))*>) by A17, FINSEQ_1:31;
then union (rng F) = (union (rng F1)) \/ (union (rng <*(F . (n + 1))*>)) by ZFMISC_1:78
.= union ((rng G1) \/ (rng <*(F . (n + 1))*>)) by A6, ZFMISC_1:78
.= union (rng G) by FINSEQ_1:31 ;
hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) ) by A50; ::_thesis: verum
end;
end;
end;
hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) ) ; ::_thesis: verum
end;
hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) ) ; ::_thesis: verum
end;
A59: len F = len F ;
A60: S1[ 0 ]
proof
let F be Finite_Sep_Sequence of S; ::_thesis: ( len F = 0 implies ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) ) )
assume A61: len F = 0 ; ::_thesis: ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) )
take G = F; ::_thesis: ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) )
G = {} by A61;
hence ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) ) ; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A60, A1);
hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) ) by A59; ::_thesis: verum
end;
Lm1: for a being FinSequence of ExtREAL
for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds
a . n = p ) holds
Sum a = N * p
proof
defpred S1[ Nat] means for F being FinSequence of ExtREAL
for p being Element of ExtREAL st $1 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = $1 & Sum F = N * p );
let a be FinSequence of ExtREAL ; ::_thesis: for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds
a . n = p ) holds
Sum a = N * p
let p, N be Element of ExtREAL ; ::_thesis: ( N = len a & ( for n being Nat st n in dom a holds
a . n = p ) implies Sum a = N * p )
assume that
A1: N = len a and
A2: for n being Nat st n in dom a holds
a . n = p ; ::_thesis: Sum a = N * p
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
for F being FinSequence of ExtREAL
for p being Element of ExtREAL st k + 1 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = k + 1 & Sum F = N * p )
proof
let F be FinSequence of ExtREAL ; ::_thesis: for p being Element of ExtREAL st k + 1 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = k + 1 & Sum F = N * p )
let p be Element of ExtREAL ; ::_thesis: ( k + 1 = len F & ( for n being Nat st n in dom F holds
F . n = p ) implies ex N being Element of ExtREAL st
( N = k + 1 & Sum F = N * p ) )
assume that
A5: k + 1 = len F and
A6: for n being Nat st n in dom F holds
F . n = p ; ::_thesis: ex N being Element of ExtREAL st
( N = k + 1 & Sum F = N * p )
F <> {} by A5;
then consider G being FinSequence, v being set such that
A7: F = G ^ <*v*> by FINSEQ_1:46;
reconsider G = G as FinSequence of ExtREAL by A7, FINSEQ_1:36;
A8: k + 1 = (len G) + (len <*v*>) by A5, A7, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
dom <*v*> = Seg 1 by FINSEQ_1:38;
then A9: 1 in dom <*v*> by FINSEQ_1:2, TARSKI:def_1;
1 <= k + 1 by NAT_1:11;
then A10: k + 1 in dom F by A5, FINSEQ_3:25;
v = <*v*> . 1 by FINSEQ_1:40
.= F . (k + 1) by A7, A8, A9, FINSEQ_1:def_7
.= p by A6, A10 ;
then reconsider v = v as Element of ExtREAL ;
consider g being Function of NAT,ExtREAL such that
A11: Sum G = g . (len G) and
A12: g . 0 = 0. and
A13: for i being Element of NAT st i < len G holds
g . (i + 1) = (g . i) + (G . (i + 1)) by EXTREAL1:def_2;
for n being Nat st n in dom G holds
G . n = p
proof
let n be Nat; ::_thesis: ( n in dom G implies G . n = p )
A14: len G <= (len G) + 1 by NAT_1:11;
assume A15: n in dom G ; ::_thesis: G . n = p
then n <= len G by FINSEQ_3:25;
then A16: n <= (len G) + 1 by A14, XXREAL_0:2;
A17: len F = (len G) + (len <*v*>) by A7, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
1 <= n by A15, FINSEQ_3:25;
then n in dom F by A16, A17, FINSEQ_3:25;
then F . n = p by A6;
hence G . n = p by A7, A15, FINSEQ_1:def_7; ::_thesis: verum
end;
then consider N1 being Element of ExtREAL such that
A18: N1 = k and
A19: Sum G = N1 * p by A4, A8;
consider f being Function of NAT,ExtREAL such that
A20: Sum F = f . (len F) and
A21: f . 0 = 0. and
A22: for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) by EXTREAL1:def_2;
A23: for k1 being Nat st k1 <= len G holds
f . k1 = g . k1
proof
defpred S2[ Nat] means ( $1 <= len G implies f . $1 = g . $1 );
A24: for k1 being Nat st S2[k1] holds
S2[k1 + 1]
proof
let k1 be Nat; ::_thesis: ( S2[k1] implies S2[k1 + 1] )
assume A25: S2[k1] ; ::_thesis: S2[k1 + 1]
reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_(_k1_+_1_<=_len_G_implies_S2[k1_+_1]_)
assume A26: k1 + 1 <= len G ; ::_thesis: S2[k1 + 1]
then A27: k1 < len G by NAT_1:13;
len F = (len G) + (len <*v*>) by A7, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
then k1 < len F by A27, NAT_1:13;
then A28: f . (k1 + 1) = (f . k1) + (F . (k1 + 1)) by A22;
1 <= k1 + 1 by NAT_1:11;
then A29: k1 + 1 in dom G by A26, FINSEQ_3:25;
( k1 <= k1 + 1 & g . (k1 + 1) = (g . k1) + (G . (k1 + 1)) ) by A13, A27, NAT_1:11;
hence S2[k1 + 1] by A7, A25, A28, A29, FINSEQ_1:def_7, XXREAL_0:2; ::_thesis: verum
end;
hence S2[k1 + 1] ; ::_thesis: verum
end;
A30: S2[ 0 ] by A21, A12;
for k1 being Nat holds S2[k1] from NAT_1:sch_2(A30, A24);
hence for k1 being Nat st k1 <= len G holds
f . k1 = g . k1 ; ::_thesis: verum
end;
take N1 + 1. ; ::_thesis: ( N1 + 1. = k + 1 & Sum F = (N1 + 1.) * p )
k < len F by A5, NAT_1:13;
then Sum F = (f . k) + (F . (k + 1)) by A5, A20, A22
.= (g . k) + (F . (k + 1)) by A8, A23 ;
then Sum F = (Sum G) + p by A6, A8, A10, A11
.= (N1 * p) + (1. * p) by A19, XXREAL_3:81 ;
hence ( N1 + 1. = k + 1 & Sum F = (N1 + 1.) * p ) by A18, SUPINF_2:1, XXREAL_3:96; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
for F being FinSequence of ExtREAL
for p being Element of ExtREAL st 0 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = 0 & Sum F = N * p )
proof
let F be FinSequence of ExtREAL ; ::_thesis: for p being Element of ExtREAL st 0 = len F & ( for n being Nat st n in dom F holds
F . n = p ) holds
ex N being Element of ExtREAL st
( N = 0 & Sum F = N * p )
let p be Element of ExtREAL ; ::_thesis: ( 0 = len F & ( for n being Nat st n in dom F holds
F . n = p ) implies ex N being Element of ExtREAL st
( N = 0 & Sum F = N * p ) )
assume that
A31: 0 = len F and
for n being Nat st n in dom F holds
F . n = p ; ::_thesis: ex N being Element of ExtREAL st
( N = 0 & Sum F = N * p )
take 0. ; ::_thesis: ( 0. = 0 & Sum F = 0. * p )
ex f being Function of NAT,ExtREAL st
( Sum F = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by EXTREAL1:def_2;
hence ( 0. = 0 & Sum F = 0. * p ) by A31; ::_thesis: verum
end;
then A32: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A32, A3);
then ex N9 being Element of ExtREAL st
( N9 = len a & Sum a = N9 * p ) by A2;
hence Sum a = N * p by A1; ::_thesis: verum
end;
Lm2: for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) & ( for x being set st x in dom f holds
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 ) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) & ( for x being set st x in dom f holds
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; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) & ( for x being set st x in dom f holds
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; ::_thesis: ( f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) & ( for x being set st x in dom f holds
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: for x being set st x in dom f holds
0. <= f . x and
A3: for x being set st x in dom f holds
0. <> f . x ; ::_thesis: 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 ) ) )
consider F1 being Finite_Sep_Sequence of S such that
A4: dom f = union (rng F1) and
A5: 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 G being Finite_Sep_Sequence of S such that
A6: union (rng F1) = union (rng G) and
A7: for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F1 & F1 . m = G . n ) ) by Th13;
set F = <*{}*> ^ G;
( rng <*{}*> = {{}} & {} in S ) by FINSEQ_1:38, MEASURE1:7;
then rng <*{}*> c= S by ZFMISC_1:31;
then (rng <*{}*>) \/ (rng G) c= S by XBOOLE_1:8;
then rng (<*{}*> ^ G) c= S by FINSEQ_1:31;
then reconsider F = <*{}*> ^ G as FinSequence of S by FINSEQ_1:def_4;
for x, y being set st x <> y holds
F . x misses F . y
proof
let x, y be set ; ::_thesis: ( x <> y implies F . x misses F . y )
assume A8: x <> y ; ::_thesis: F . x misses F . y
now__::_thesis:_(_(_x_in_dom_F_&_y_in_dom_F_&_F_._x_misses_F_._y_)_or_(_(_not_x_in_dom_F_or_not_y_in_dom_F_)_&_F_._x_misses_F_._y_)_)
percases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ;
caseA9: ( x in dom F & y in dom F ) ; ::_thesis: F . x misses F . y
then reconsider x = x, y = y as Element of NAT ;
A10: x in Seg (len (<*{}*> ^ G)) by A9, FINSEQ_1:def_3;
then A11: x <= len (<*{}*> ^ G) by FINSEQ_1:1;
A12: y in Seg (len (<*{}*> ^ G)) by A9, FINSEQ_1:def_3;
then A13: 1 <= y by FINSEQ_1:1;
A14: y <= len (<*{}*> ^ G) by A12, FINSEQ_1:1;
A15: 1 <= x by A10, FINSEQ_1:1;
now__::_thesis:_(_(_(_x_=_1_or_y_=_1_)_&_F_._x_misses_F_._y_)_or_(_x_<>_1_&_y_<>_1_&_F_._x_misses_F_._y_)_)
percases ( x = 1 or y = 1 or ( x <> 1 & y <> 1 ) ) ;
caseA16: ( x = 1 or y = 1 ) ; ::_thesis: F . x misses F . y
A17: dom <*{}*> = Seg 1 by FINSEQ_1:38;
now__::_thesis:_(_(_x_=_1_&_F_._x_misses_F_._y_)_or_(_y_=_1_&_F_._x_misses_F_._y_)_)
percases ( x = 1 or y = 1 ) by A16;
caseA18: x = 1 ; ::_thesis: F . x misses F . y
then x in dom <*{}*> by A17, FINSEQ_1:2, TARSKI:def_1;
then F . x = <*{}*> . x by FINSEQ_1:def_7;
then F . x = {} by A18, FINSEQ_1:def_8;
hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum
end;
caseA19: y = 1 ; ::_thesis: F . x misses F . y
then y in dom <*{}*> by A17, FINSEQ_1:2, TARSKI:def_1;
then F . y = <*{}*> . y by FINSEQ_1:def_7;
then F . y = {} by A19, FINSEQ_1:def_8;
hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence F . x misses F . y ; ::_thesis: verum
end;
caseA20: ( x <> 1 & y <> 1 ) ; ::_thesis: F . x misses F . y
then 1 < y by A13, XXREAL_0:1;
then len <*{}*> < y by FINSEQ_1:40;
then A21: F . y = G . (y - (len <*{}*>)) by A14, FINSEQ_1:24;
1 < x by A15, A20, XXREAL_0:1;
then len <*{}*> < x by FINSEQ_1:40;
then A22: F . x = G . (x - (len <*{}*>)) by A11, FINSEQ_1:24;
x - (len <*{}*>) <> y - (len <*{}*>) by A8;
hence F . x misses F . y by A22, A21, PROB_2:def_2; ::_thesis: verum
end;
end;
end;
hence F . x misses F . y ; ::_thesis: verum
end;
case ( not x in dom F or not y in dom F ) ; ::_thesis: F . x misses F . y
then ( F . x = {} or F . y = {} ) by FUNCT_1:def_2;
hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence F . x misses F . y ; ::_thesis: verum
end;
then reconsider F = F as Finite_Sep_Sequence of S by PROB_2:def_2;
A23: union (rng F) = union ((rng <*{}*>) \/ (rng G)) by FINSEQ_1:31
.= union ({{}} \/ (rng G)) by FINSEQ_1:38
.= (union {{}}) \/ (union (rng G)) by ZFMISC_1:78
.= {} \/ (union (rng G)) by ZFMISC_1:25
.= dom f by A4, A6 ;
defpred S1[ Nat, Element of ExtREAL ] means ( ( for x being Element of X st $1 in dom F & $1 = 1 holds
$2 = 0. ) & ( for x being Element of X st $1 in dom F & $1 >= 2 & x in F . $1 holds
$2 = f . x ) );
A24: for k being Nat st k in Seg (len F) holds
ex y being Element of ExtREAL st S1[k,y]
proof
let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of ExtREAL st S1[k,y] )
assume A25: k in Seg (len F) ; ::_thesis: ex y being Element of ExtREAL st S1[k,y]
ex y being Element of ExtREAL st S1[k,y]
proof
now__::_thesis:_(_(_k_=_1_&_ex_y_being_Element_of_ExtREAL_ex_y_being_Element_of_ExtREAL_st_S1[k,y]_)_or_(_k_<>_1_&_ex_y_being_Element_of_ExtREAL_ex_y_being_Element_of_ExtREAL_st_S1[k,y]_)_)
percases ( k = 1 or k <> 1 ) ;
caseA26: k = 1 ; ::_thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S1[k,y]
take y = 0. ; ::_thesis: ex y being Element of ExtREAL st S1[k,y]
( ( for x being Element of X st k in dom F & k = 1 holds
y = 0. ) & ( for x being Element of X st k in dom F & k >= 2 & x in F . k holds
y = f . x ) ) by A26;
hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum
end;
caseA27: k <> 1 ; ::_thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S1[k,y]
A28: k <= len F by A25, FINSEQ_1:1;
then k <= (len <*{}*>) + (len G) by FINSEQ_1:22;
then A29: k - (len <*{}*>) <= len G by XREAL_1:20;
1 <= k by A25, FINSEQ_1:1;
then 1 < k by A27, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then A30: (len <*{}*>) + 1 <= k by FINSEQ_1:39;
then consider k2 being Nat such that
A31: ((len <*{}*>) + 1) + k2 = k by NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def_12;
1 + k2 = k - (len <*{}*>) by A31;
then 1 <= 1 + k2 by A30, XREAL_1:19;
then 1 + k2 in Seg (len G) by A31, A29, FINSEQ_1:1;
then A32: 1 + k2 in dom G by FINSEQ_1:def_3;
then consider m1 being Nat such that
A33: m1 in dom F1 and
A34: F1 . m1 = G . (1 + k2) by A7;
k <= (len <*{}*>) + (len G) by A28, FINSEQ_1:22;
then A35: F . k = G . (k - (len <*{}*>)) by A30, FINSEQ_1:23
.= G . (1 + k2) by A31 ;
then F . k <> {} by A7, A32;
then consider z being set such that
A36: z in F . k by XBOOLE_0:def_1;
take y = f . z; ::_thesis: ex y being Element of ExtREAL st S1[k,y]
F . k in rng F1 by A35, A33, A34, FUNCT_1:3;
then F . k in S ;
then reconsider z = z as Element of X by A36;
A37: for x being Element of X st k in dom F & k >= 2 & x in F . k holds
y = f . x
proof
let x be Element of X; ::_thesis: ( k in dom F & k >= 2 & x in F . k implies y = f . x )
assume that
k in dom F and
k >= 2 and
A38: x in F . k ; ::_thesis: y = f . x
z in F1 . m1 by A35, A36, A34;
hence y = f . x by A5, A35, A33, A34, A38; ::_thesis: verum
end;
for x being Element of X st k in dom F & k = 1 holds
y = 0. by A27;
hence ex y being Element of ExtREAL st S1[k,y] by A37; ::_thesis: verum
end;
end;
end;
hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum
end;
hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum
end;
consider a being FinSequence of ExtREAL such that
A39: ( dom a = Seg (len F) & ( for n being Nat st n in Seg (len F) holds
S1[n,a . n] ) ) from FINSEQ_1:sch_5(A24);
A40: dom F = dom a by A39, FINSEQ_1:def_3;
A41: for n being Nat
for x being Element of X st n in dom F & n >= 2 & x in F . n holds
a . n = f . x
proof
let n be Nat; ::_thesis: for x being Element of X st n in dom F & n >= 2 & x in F . n holds
a . n = f . x
let x be Element of X; ::_thesis: ( n in dom F & n >= 2 & x in F . n implies a . n = f . x )
assume that
A42: n in dom F and
A43: ( n >= 2 & x in F . n ) ; ::_thesis: a . n = f . x
n in Seg (len F) by A42, FINSEQ_1:def_3;
hence a . n = f . x by A39, A42, A43; ::_thesis: verum
end;
A44: for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty )
proof
let n be Nat; ::_thesis: ( 2 <= n & n in dom a implies ( 0. < a . n & a . n < +infty ) )
assume that
A45: 2 <= n and
A46: n in dom a ; ::_thesis: ( 0. < a . n & a . n < +infty )
1 + 1 <= n by A45;
then A47: (len <*{}*>) + 1 <= n by FINSEQ_1:39;
n <= len F by A39, A46, FINSEQ_1:1;
then n <= (len <*{}*>) + (len G) by FINSEQ_1:22;
then A48: F . n = G . (n - (len <*{}*>)) by A47, FINSEQ_1:23
.= G . (n - 1) by FINSEQ_1:39 ;
( dom <*{}*> = {1} & 1 <> n ) by A45, FINSEQ_1:2, FINSEQ_1:38;
then not n in dom <*{}*> by TARSKI:def_1;
then consider k being Nat such that
A49: k in dom G and
A50: n = (len <*{}*>) + k by A40, A46, FINSEQ_1:25;
n = 1 + k by A50, FINSEQ_1:39;
then F . n <> {} by A7, A48, A49;
then consider x1 being set such that
A51: x1 in F . n by XBOOLE_0:def_1;
A52: F . n c= union (rng F) by A40, A46, FUNCT_1:3, ZFMISC_1:74;
then x1 in dom f by A23, A51;
then reconsider x1 = x1 as Element of X ;
A53: 0. <> f . x1 by A3, A23, A51, A52;
f is V73() by A1, MESFUNC2:def_4;
then A54: |.(f . x1).| < +infty by A23, A51, A52, MESFUNC2:def_1;
a . n = f . x1 by A41, A40, A45, A46, A51;
hence ( 0. < a . n & a . n < +infty ) by A2, A23, A51, A52, A54, A53, EXTREAL2:10; ::_thesis: verum
end;
take F ; ::_thesis: 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 ; ::_thesis: ( 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 ) ) )
A55: for n9 being Nat st n9 in dom F holds
for x being set st x in F . n9 holds
f . x = a . n9
proof
let n9 be Nat; ::_thesis: ( n9 in dom F implies for x being set st x in F . n9 holds
f . x = a . n9 )
assume A56: n9 in dom F ; ::_thesis: for x being set st x in F . n9 holds
f . x = a . n9
now__::_thesis:_(_(_n9_=_1_&_(_for_x_being_set_st_x_in_F_._n9_holds_
f_._x_=_a_._n9_)_)_or_(_n9_<>_1_&_(_for_x_being_set_st_x_in_F_._n9_holds_
f_._x_=_a_._n9_)_)_)
percases ( n9 = 1 or n9 <> 1 ) ;
caseA57: n9 = 1 ; ::_thesis: for x being set st x in F . n9 holds
f . x = a . n9
thus for x being set st x in F . n9 holds
f . x = a . n9 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in F . n9 implies f . x = a . n9 )
dom <*{}*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then 1 in dom <*{}*> by TARSKI:def_1;
then A58: F . 1 = <*{}*> . 1 by FINSEQ_1:def_7
.= {} by FINSEQ_1:40 ;
assume x in F . n9 ; ::_thesis: f . x = a . n9
hence f . x = a . n9 by A57, A58; ::_thesis: verum
end;
end;
caseA59: n9 <> 1 ; ::_thesis: for x being set st x in F . n9 holds
f . x = a . n9
n9 in Seg (len F) by A56, FINSEQ_1:def_3;
then 1 <= n9 by FINSEQ_1:1;
then 1 < n9 by A59, XXREAL_0:1;
then A60: 1 + 1 <= n9 by NAT_1:13;
thus for x being set st x in F . n9 holds
f . x = a . n9 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in F . n9 implies f . x = a . n9 )
assume A61: x in F . n9 ; ::_thesis: f . x = a . n9
F . n9 in rng F by A56, FUNCT_1:3;
then F . n9 in S ;
then reconsider x = x as Element of X by A61;
a . n9 = f . x by A41, A56, A60, A61;
hence f . x = a . n9 ; ::_thesis: verum
end;
end;
end;
end;
hence for x being set st x in F . n9 holds
f . x = a . n9 ; ::_thesis: verum
end;
len F = (len <*{}*>) + (len G) by FINSEQ_1:22
.= 1 + (len G) by FINSEQ_1:39 ;
then 1 <= len F by NAT_1:11;
then 1 in Seg (len F) by FINSEQ_1:1;
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 A23, A39, A40, A55, A44, Def1; ::_thesis: verum
end;
Lm3: for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) & 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 ) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) & 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; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) & 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; ::_thesis: ( f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) & 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: for x being set st x in dom f holds
0. <= f . x and
A3: ex x being set st
( x in dom f & 0. = f . x ) ; ::_thesis: 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 ) ) )
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 set 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 set 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
proof
let F9 be set ; ::_thesis: ( 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. ) ) } implies F9 in bool X )
assume 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. ) ) } ; ::_thesis: F9 in bool X
then ex Fn being Element of S st
( F9 = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) ;
hence F9 in bool X ; ::_thesis: verum
end;
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. ) )
proof
F1 . n0 in rng F1 by A10, FUNCT_1:3;
hence F1 . n0 is Element of S ; ::_thesis: ( F1 . n0 in rng F1 & ( for x being Element of X st x in F1 . n0 holds
f . x = 0. ) )
thus F1 . n0 in rng F1 by A10, FUNCT_1:3; ::_thesis: for x being Element of X st x in F1 . n0 holds
f . x = 0.
let x be Element of X; ::_thesis: ( x in F1 . n0 implies f . x = 0. )
assume x in F1 . n0 ; ::_thesis: f . x = 0.
hence f . x = 0. by A5, A7, A8, A10, A11; ::_thesis: verum
end;
then A13: F1 . n0 in F0 ;
for z being set st z in F0 holds
z in rng F1
proof
let z be set ; ::_thesis: ( z in F0 implies z in rng F1 )
assume z in F0 ; ::_thesis: z in rng F1
then ex Fn9 being Element of S st
( z = Fn9 & Fn9 in rng F1 & ( for x being Element of X st x in Fn9 holds
f . x = 0. ) ) ;
hence z in rng F1 ; ::_thesis: verum
end;
then A14: F0 c= rng F1 by TARSKI:def_3;
for z being set 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
proof
let z be set ; ::_thesis: ( 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. ) ) } implies z in dom F1 )
assume 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. ) ) } ; ::_thesis: z in dom F1
then ex n9 being Element of NAT st
( z = n9 & n9 in dom F1 & ( for x being Element of X st x in F1 . n9 holds
f . x = 0. ) ) ;
hence z in dom F1 ; ::_thesis: verum
end;
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 by TARSKI:def_3;
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 set st F9 in F0 holds
F9 in S
proof
let F9 be set ; ::_thesis: ( F9 in F0 implies F9 in S )
assume F9 in F0 ; ::_thesis: F9 in S
then ex Fn being Element of S st
( F9 = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) ;
hence F9 in S ; ::_thesis: verum
end;
then F0 c= S by TARSKI:def_3;
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; ::_thesis: ( k in Seg lenF implies ex U being Element of S st S1[k,U] )
assume A25: k in Seg lenF ; ::_thesis: ex U being Element of S st S1[k,U]
percases ( k = 1 or k <> 1 ) ;
supposeA26: k = 1 ; ::_thesis: ex U being Element of S st S1[k,U]
take G1 ; ::_thesis: S1[k,G1]
thus S1[k,G1] by A26; ::_thesis: verum
end;
supposeA27: k <> 1 ; ::_thesis: 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 ; ::_thesis: S1[k,U]
thus S1[k,U] by A27, A29; ::_thesis: 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; ::_thesis: ( k in Seg (len F) implies ex x being Element of ExtREAL st S2[k,x] )
assume A33: k in Seg (len F) ; ::_thesis: ex x being Element of ExtREAL st S2[k,x]
then A34: k in dom F by FINSEQ_1:def_3;
now__::_thesis:_(_(_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]_)_)
percases ( k = 1 or k <> 1 ) ;
caseA35: k = 1 ; ::_thesis: ex x being Element of ExtREAL ex x being Element of ExtREAL st S2[k,x]
take x = 0. ; ::_thesis: ex x being Element of ExtREAL st S2[k,x]
A36: F . k = G1 by A31, A34, A35;
for y being Element of X holds
( ( y in F . k implies 0. = f . y ) & ( F . k = {} implies 0. = 1. ) )
proof
let y be Element of X; ::_thesis: ( ( y in F . k implies 0. = f . y ) & ( F . k = {} implies 0. = 1. ) )
( y in F . k implies 0. = f . y )
proof
assume y in F . k ; ::_thesis: 0. = f . y
then consider Y being set such that
A37: y in Y and
A38: Y in F0 by A36, TARSKI:def_4;
ex Fn being Element of S st
( Y = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) by A38;
hence 0. = f . y by A37; ::_thesis: verum
end;
hence ( ( y in F . k implies 0. = f . y ) & ( F . k = {} implies 0. = 1. ) ) by A8, A11, A13, A36, TARSKI:def_4; ::_thesis: verum
end;
hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: verum
end;
caseA39: k <> 1 ; ::_thesis: 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;
now__::_thesis:_(_(_F_._k_=_{}_&_ex_x_being_Element_of_ExtREAL_ex_x_being_Element_of_ExtREAL_st_S2[k,x]_)_or_(_F_._k_<>_{}_&_ex_x_being_Element_of_ExtREAL_ex_x_being_Element_of_ExtREAL_st_S2[k,x]_)_)
percases ( F . k = {} or F . k <> {} ) ;
caseA46: F . k = {} ; ::_thesis: ex x being Element of ExtREAL ex x being Element of ExtREAL st S2[k,x]
take x = 1. ; ::_thesis: ex x being Element of ExtREAL st S2[k,x]
for y being Element of X holds
( ( y in F . k implies 1. = f . y ) & ( F . k = {} implies 1. = 1. ) ) by A46;
hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: verum
end;
case F . k <> {} ; ::_thesis: ex x being Element of ExtREAL ex x being Element of ExtREAL st S2[k,x]
then consider y1 being set such that
A47: y1 in F . k by XBOOLE_0:def_1;
F . k in rng F by A34, FUNCT_1:3;
then F . k in S ;
then reconsider y1 = y1 as Element of X by A47;
take x = f . y1; ::_thesis: ex x being Element of ExtREAL st S2[k,x]
for y being Element of X holds
( ( y in F . k implies x = f . y ) & ( F . k = {} implies x = 1. ) ) by A7, A44, A45, A47;
hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: verum
end;
end;
end;
hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: verum
end;
end;
end;
hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: 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
proof
let n be Nat; ::_thesis: for x being Element of X st n in dom F & x in F . n holds
a . n = f . x
let x be Element of X; ::_thesis: ( n in dom F & x in F . n implies a . n = f . x )
assume that
A50: n in dom F and
A51: x in F . n ; ::_thesis: a . n = f . x
n in Seg (len F) by A50, FINSEQ_1:def_3;
hence a . n = f . x by A48, A51; ::_thesis: verum
end;
A52: for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n
proof
let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds
f . x = a . n )
assume A53: n in dom F ; ::_thesis: for x being set st x in F . n holds
f . x = a . n
let x be set ; ::_thesis: ( x in F . n implies f . x = a . n )
assume A54: x in F . n ; ::_thesis: f . x = a . n
F . n in rng F by A53, FUNCT_1:3;
then F . n in S ;
then reconsider x = x as Element of X by A54;
a . n = f . x by A49, A53, A54;
hence f . x = a . n ; ::_thesis: verum
end;
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; ::_thesis: ( 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; ::_thesis: 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; ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: 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) <> {} ; ::_thesis: contradiction
then consider v being set 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 set 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)) = {} by XBOOLE_0:def_7;
hence contradiction by A69, A73, A74, A76, A80, XBOOLE_0:def_4; ::_thesis: verum
end;
hence F . n misses F . m by XBOOLE_0:def_7; ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: 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; ::_thesis: verum
end;
A97: for x, y being set st x <> y holds
F . x misses F . y
proof
let x, y be set ; ::_thesis: ( x <> y implies F . x misses F . y )
assume A98: x <> y ; ::_thesis: F . x misses F . y
now__::_thesis:_(_(_x_in_dom_F_&_y_in_dom_F_&_F_._x_misses_F_._y_)_or_(_(_not_x_in_dom_F_or_not_y_in_dom_F_)_&_F_._x_misses_F_._y_)_)
percases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ;
caseA99: ( x in dom F & y in dom F ) ; ::_thesis: F . x misses F . y
then reconsider x = x, y = y as Element of NAT ;
now__::_thesis:_(_(_(_x_=_1_or_y_=_1_)_&_F_._x_misses_F_._y_)_or_(_x_<>_1_&_y_<>_1_&_F_._x_misses_F_._y_)_)
percases ( x = 1 or y = 1 or ( x <> 1 & y <> 1 ) ) ;
case ( x = 1 or y = 1 ) ; ::_thesis: F . x misses F . y
hence F . x misses F . y by A60, A98, A99; ::_thesis: verum
end;
case ( x <> 1 & y <> 1 ) ; ::_thesis: F . x misses F . y
hence F . x misses F . y by A81, A98, A99; ::_thesis: verum
end;
end;
end;
hence F . x misses F . y ; ::_thesis: verum
end;
caseA100: ( not x in dom F or not y in dom F ) ; ::_thesis: F . x misses F . y
now__::_thesis:_(_(_not_x_in_dom_F_&_F_._x_misses_F_._y_)_or_(_not_y_in_dom_F_&_F_._x_misses_F_._y_)_)
percases ( not x in dom F or not y in dom F ) by A100;
case not x in dom F ; ::_thesis: F . x misses F . y
then F . x = {} by FUNCT_1:def_2;
hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum
end;
case not y in dom F ; ::_thesis: F . x misses F . y
then F . y = {} by FUNCT_1:def_2;
hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence F . x misses F . y ; ::_thesis: verum
end;
end;
end;
hence F . x misses F . y ; ::_thesis: verum
end;
for z being set st z in union (rng F) holds
z in union (rng F1)
proof
let z be set ; ::_thesis: ( z in union (rng F) implies z in union (rng F1) )
assume z in union (rng F) ; ::_thesis: 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 set 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__::_thesis:_(_(_k_=_1_&_z_in_union_(rng_F1)_)_or_(_k_<>_1_&_z_in_union_(rng_F1)_)_)
percases ( k = 1 or k <> 1 ) ;
case k = 1 ; ::_thesis: z in union (rng F1)
then z in G1 by A31, A101, A103, A104;
then consider Y9 being set such that
A105: z in Y9 and
A106: Y9 in F0 by TARSKI:def_4;
ex Fn9 being Element of S st
( Y9 = Fn9 & Fn9 in rng F1 & ( for x being Element of X st x in Fn9 holds
f . x = 0. ) ) by A106;
hence z in union (rng F1) by A105, TARSKI:def_4; ::_thesis: verum
end;
caseA107: k <> 1 ; ::_thesis: 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; ::_thesis: verum
end;
end;
end;
hence z in union (rng F1) ; ::_thesis: verum
end;
then A112: union (rng F) c= union (rng F1) by TARSKI:def_3;
for z being set st z in union (rng F1) holds
z in union (rng F)
proof
let z be set ; ::_thesis: ( z in union (rng F1) implies z in union (rng F) )
assume z in union (rng F1) ; ::_thesis: 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 set 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__::_thesis:_(_(_m1_in_N_&_z_in_union_(rng_F)_)_or_(_not_m1_in_N_&_z_in_union_(rng_F)_)_)
percases ( m1 in N or not m1 in N ) ;
case m1 in N ; ::_thesis: z in union (rng F)
then ex m19 being Element of NAT st
( m1 = m19 & m19 in dom F1 & ( for x being Element of X st x in F1 . m19 holds
f . x = 0. ) ) ;
then Y in F0 by A114, A116;
then A117: z in union F0 by A113, TARSKI:def_4;
lenF >= 1 + 0 by A21, A23, XREAL_1:19;
then A118: 1 in Seg lenF by FINSEQ_1:1;
then F . 1 in rng F by A31, FUNCT_1:3;
then union F0 in rng F by A31, A118;
hence z in union (rng F) by A117, TARSKI:def_4; ::_thesis: verum
end;
case not m1 in N ; ::_thesis: z in union (rng F)
then m1 in (findom F1) \ N by A115, XBOOLE_0:def_5;
then consider m19 being set 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; ::_thesis: verum
end;
end;
end;
hence z in union (rng F) ; ::_thesis: verum
end;
then union (rng F1) c= union (rng F) by TARSKI:def_3;
then A126: union (rng F) = dom f by A6, A112, XBOOLE_0:def_10;
reconsider F = F as Finite_Sep_Sequence of S by A97, PROB_2:def_2;
take F ; ::_thesis: 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 ; ::_thesis: ( 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 V73() 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; ::_thesis: ( 2 <= n & n in dom a implies ( 0. < a . n & a . n < +infty ) )
assume that
A129: 2 <= n and
A130: n in dom a ; ::_thesis: ( 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
percases ( F . n <> {} or F . n = {} ) ;
supposeA136: F . n <> {} ; ::_thesis: ( 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 set 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, XBOOLE_0:def_7;
then A140: not y in G1 by A138, XBOOLE_0:def_4;
thus a . n <> 0. ::_thesis: ( 0. <= a . n & a . n < +infty )
proof
assume a . n = 0. ; ::_thesis: contradiction
then for x being Element of X st x in F . n holds
f . x = 0. by A56, A130;
then Fn in F0 by A134;
hence contradiction by A138, A140, TARSKI:def_4; ::_thesis: verum
end;
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 A2, A6, A112, A139, A141, EXTREAL2:10; ::_thesis: verum
end;
supposeA142: F . n = {} ; ::_thesis: ( a . n <> 0. & 0. <= a . n & a . n < +infty )
hence a . n <> 0. by A48, A130; ::_thesis: ( 0. <= a . n & a . n < +infty )
thus 0. <= a . n by A48, A130, A142; ::_thesis: a . n < +infty
S2[n,a . n] by A48, A130;
hence a . n < +infty by A142, XXREAL_0:9; ::_thesis: verum
end;
end;
end;
hence ( 0. < a . n & a . n < +infty ) ; ::_thesis: 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, Def1; ::_thesis: verum
end;
theorem Th14: :: MESFUNC3:14
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
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 ) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
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; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
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; ::_thesis: ( f is_simple_func_in S & ( for x being set st x in dom f holds
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 A1: ( f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) ) ; ::_thesis: 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 ) ) )
percases ( ex x being set st
( x in dom f & 0. = f . x ) or for x being set st x in dom f holds
0. <> f . x ) ;
suppose ex x being set st
( x in dom f & 0. = f . x ) ; ::_thesis: 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 ) ) )
hence 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 ) ) ) by A1, Lm3; ::_thesis: verum
end;
suppose for x being set st x in dom f holds
0. <> f . x ; ::_thesis: 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 ) ) )
hence 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 ) ) ) by A1, Lm2; ::_thesis: verum
end;
end;
end;
theorem :: MESFUNC3:15
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let f be PartFunc of X,ExtREAL; ::_thesis: for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let F be Finite_Sep_Sequence of S; ::_thesis: for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let a be FinSequence of ExtREAL ; ::_thesis: for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let x be Element of X; ::_thesis: ( F,a are_Re-presentation_of f & x in dom f implies ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) )
assume that
A1: F,a are_Re-presentation_of f and
A2: x in dom f ; ::_thesis: ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
A3: dom F = dom a by A1, Def1;
deffunc H1( Nat) -> Element of ExtREAL = (a . $1) * ((chi ((F . $1),X)) . x);
consider ax being FinSequence of ExtREAL such that
A4: ( len ax = len a & ( for j being Nat st j in dom ax holds
ax . j = H1(j) ) ) from FINSEQ_2:sch_1();
A5: dom ax = Seg (len a) by A4, FINSEQ_1:def_3;
A6: dom f = union (rng F) by A1, Def1;
A7: f . x = Sum ax
proof
consider Y being set such that
A8: x in Y and
A9: Y in rng F by A2, A6, TARSKI:def_4;
consider k being set such that
A10: k in dom F and
A11: Y = F . k by A9, FUNCT_1:def_3;
reconsider k = k as Element of NAT by A10;
A12: k in Seg (len a) by A3, A10, FINSEQ_1:def_3;
then A13: len ax >= k by A4, FINSEQ_1:1;
A14: for i being Nat st i in Seg (len ax) & i <> k holds
ax . i = 0.
proof
let i be Nat; ::_thesis: ( i in Seg (len ax) & i <> k implies ax . i = 0. )
assume that
A15: i in Seg (len ax) and
A16: i <> k ; ::_thesis: ax . i = 0.
F . i misses F . k by A16, PROB_2:def_2;
then (F . i) /\ (F . k) = {} by XBOOLE_0:def_7;
then not x in F . i by A8, A11, XBOOLE_0:def_4;
then A17: (chi ((F . i),X)) . x = 0. by FUNCT_3:def_3;
ax . i = (a . i) * ((chi ((F . i),X)) . x) by A4, A5, A15;
hence ax . i = 0. by A17; ::_thesis: verum
end;
consider SA being Function of NAT,ExtREAL such that
A18: Sum ax = SA . (len ax) and
A19: SA . 0 = 0. and
A20: for i being Element of NAT st i < len ax holds
SA . (i + 1) = (SA . i) + (ax . (i + 1)) by EXTREAL1:def_2;
defpred S1[ Nat] means ( $1 <= len ax implies ( ( $1 < k implies SA . $1 = 0. ) & ( $1 >= k implies SA . $1 = f . x ) ) );
A21: for i being Nat st i in Seg (len ax) & i = k holds
ax . i = f . x
proof
let i be Nat; ::_thesis: ( i in Seg (len ax) & i = k implies ax . i = f . x )
assume that
A22: i in Seg (len ax) and
A23: i = k ; ::_thesis: ax . i = f . x
(chi ((F . i),X)) . x = 1. by A8, A11, A23, FUNCT_3:def_3;
then ax . i = (a . i) * 1. by A4, A5, A22
.= a . i by XXREAL_3:81 ;
hence ax . i = f . x by A1, A8, A10, A11, A23, Def1; ::_thesis: verum
end;
A24: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A25: S1[i] ; ::_thesis: S1[i + 1]
assume A26: i + 1 <= len ax ; ::_thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )
reconsider i = i as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_(_(_i_+_1_<_k_&_(_i_+_1_<_k_implies_SA_._(i_+_1)_=_0._)_&_(_i_+_1_>=_k_implies_SA_._(i_+_1)_=_f_._x_)_)_or_(_i_+_1_>=_k_&_(_i_+_1_<_k_implies_SA_._(i_+_1)_=_0._)_&_(_i_+_1_>=_k_implies_SA_._(i_+_1)_=_f_._x_)_)_)
percases ( i + 1 < k or i + 1 >= k ) ;
caseA27: i + 1 < k ; ::_thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )
A28: k <= len a by A12, FINSEQ_1:1;
A29: i <= i + 1 by NAT_1:11;
then i < k by A27, XXREAL_0:2;
then A30: i < len ax by A4, A28, XXREAL_0:2;
then ( 1 <= i + 1 & i + 1 <= len ax ) by NAT_1:11, NAT_1:13;
then A31: i + 1 in Seg (len ax) by FINSEQ_1:1;
SA . (i + 1) = 0. + (ax . (i + 1)) by A20, A25, A27, A29, A30, XXREAL_0:2
.= ax . (i + 1) by XXREAL_3:4
.= 0. by A14, A27, A31 ;
hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) by A27; ::_thesis: verum
end;
caseA32: i + 1 >= k ; ::_thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )
now__::_thesis:_(_(_k_=_i_+_1_&_SA_._(i_+_1)_=_f_._x_)_or_(_k_<>_i_+_1_&_SA_._(i_+_1)_=_f_._x_)_)
percases ( k = i + 1 or k <> i + 1 ) ;
caseA33: k = i + 1 ; ::_thesis: SA . (i + 1) = f . x
A34: k <= len a by A12, FINSEQ_1:1;
then i < len ax by A4, A33, NAT_1:13;
hence SA . (i + 1) = (SA . i) + (ax . (i + 1)) by A20
.= ax . k by A4, A25, A33, A34, NAT_1:13, XXREAL_3:4
.= f . x by A4, A12, A21 ;
::_thesis: verum
end;
case k <> i + 1 ; ::_thesis: SA . (i + 1) = f . x
then A35: k < i + 1 by A32, XXREAL_0:1;
1 <= i + 1 by NAT_1:11;
then A36: i + 1 in Seg (len ax) by A26, FINSEQ_1:1;
i < len ax by A26, NAT_1:13;
hence SA . (i + 1) = (SA . i) + (ax . (i + 1)) by A20
.= (f . x) + 0. by A14, A25, A26, A35, A36, NAT_1:13
.= f . x by XXREAL_3:4 ;
::_thesis: verum
end;
end;
end;
hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) by A32; ::_thesis: verum
end;
end;
end;
hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) ; ::_thesis: verum
end;
A37: S1[ 0 ] by A12, A19, FINSEQ_1:1;
for i being Nat holds S1[i] from NAT_1:sch_2(A37, A24);
hence f . x = Sum ax by A18, A13; ::_thesis: verum
end;
take ax ; ::_thesis: ( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
dom ax = Seg (len a) by A4, FINSEQ_1:def_3;
hence ( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) by A4, A7, FINSEQ_1:def_3; ::_thesis: verum
end;
theorem :: MESFUNC3:16
for p being FinSequence of ExtREAL
for q being FinSequence of REAL st p = q holds
Sum p = Sum q by Th2;
theorem Th17: :: MESFUNC3:17
for p being FinSequence of ExtREAL st not -infty in rng p & +infty in rng p holds
Sum p = +infty
proof
let p be FinSequence of ExtREAL ; ::_thesis: ( not -infty in rng p & +infty in rng p implies Sum p = +infty )
assume A0: not -infty in rng p ; ::_thesis: ( not +infty in rng p or Sum p = +infty )
assume +infty in rng p ; ::_thesis: Sum p = +infty
then ex n being set st
( n in dom p & p . n = +infty ) by FUNCT_1:def_3;
then consider m being Nat such that
A3: m in dom p and
A4: p . m = +infty ;
m in Seg (len p) by A3, FINSEQ_1:def_3;
then A5: len p >= m by FINSEQ_1:1;
consider f being Function of NAT,ExtREAL such that
A6: Sum p = f . (len p) and
A7: f . 0 = 0. and
A8: for i being Element of NAT st i < len p holds
f . (i + 1) = (f . i) + (p . (i + 1)) by EXTREAL1:def_2;
A1: for n being Nat st n in dom p holds
-infty < p . n
proof
let n be Nat; ::_thesis: ( n in dom p implies -infty < p . n )
assume n in dom p ; ::_thesis: -infty < p . n
then p . n in rng p by FUNCT_1:def_3;
hence -infty < p . n by A0, XXREAL_0:6; ::_thesis: verum
end;
defpred S1[ Nat] means ( $1 <= len p implies ( ( $1 < m implies -infty < f . $1 ) & ( $1 >= m implies f . $1 = +infty ) ) );
A9: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A10: S1[i] ; ::_thesis: S1[i + 1]
assume A11: i + 1 <= len p ; ::_thesis: ( ( i + 1 < m implies -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) )
reconsider i = i as Element of NAT by ORDINAL1:def_12;
B01: i < len p by A11, NAT_1:13;
now__::_thesis:_(_(_i_+_1_<_m_&_-infty_<_f_._(i_+_1)_)_or_(_i_+_1_>=_m_&_(_i_+_1_<_m_implies_-infty_<_f_._(i_+_1)_)_&_(_i_+_1_>=_m_implies_f_._(i_+_1)_=_+infty_)_)_)
percases ( i + 1 < m or i + 1 >= m ) ;
case i + 1 < m ; ::_thesis: -infty < f . (i + 1)
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (len p) by A11, FINSEQ_1:1;
then i + 1 in dom p by FINSEQ_1:def_3;
then A13: -infty < p . (i + 1) by A1;
B02: -infty + -infty = -infty by XXREAL_3:def_2;
-infty + -infty < (f . i) + (p . (i + 1)) by A10, A11, NAT_1:13, A13, XXREAL_3:64;
hence -infty < f . (i + 1) by A8, B01, B02; ::_thesis: verum
end;
caseA14: i + 1 >= m ; ::_thesis: ( ( i + 1 < m implies -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) )
now__::_thesis:_(_(_i_+_1_=_m_&_f_._(i_+_1)_=_+infty_)_or_(_i_+_1_<>_m_&_f_._(i_+_1)_=_+infty_)_)
percases ( i + 1 = m or i + 1 <> m ) ;
caseA15: i + 1 = m ; ::_thesis: f . (i + 1) = +infty
f . (i + 1) = (f . i) + (p . (i + 1)) by A8, B01;
hence f . (i + 1) = +infty by A4, A10, A11, A15, NAT_1:13, XXREAL_3:def_2; ::_thesis: verum
end;
caseA16: i + 1 <> m ; ::_thesis: f . (i + 1) = +infty
i < len p by A11, NAT_1:13;
then A17: f . (i + 1) = (f . i) + (p . (i + 1)) by A8;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (len p) by A11, FINSEQ_1:1;
then i + 1 in dom p by FINSEQ_1:def_3;
then A18: p . (i + 1) <> -infty by A1;
i + 1 > m by A14, A16, XXREAL_0:1;
hence f . (i + 1) = +infty by A10, A11, A18, A17, NAT_1:13, XXREAL_3:def_2; ::_thesis: verum
end;
end;
end;
hence ( ( i + 1 < m implies -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) ; ::_thesis: verum
end;
end;
end;
hence ( ( i + 1 < m implies -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) ; ::_thesis: verum
end;
A19: S1[ 0 ] by A3, A7, FINSEQ_3:25;
for i being Nat holds S1[i] from NAT_1:sch_2(A19, A9);
hence Sum p = +infty by A6, A5; ::_thesis: verum
end;
definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
assume A1: ( f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) ) ;
func integral (X,S,M,f) -> Element of ExtREAL means :: MESFUNC3:def 2
ex F being Finite_Sep_Sequence of S ex a, x 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 ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & it = Sum x );
existence
ex b1 being Element of ExtREAL ex F being Finite_Sep_Sequence of S ex a, x 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 ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & b1 = Sum x )
proof
consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A2: ( 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 A1, Th14;
defpred S1[ set ] means $1 in dom F;
deffunc H1( set ) -> Element of ExtREAL = (a . $1) * ((M * F) . $1);
A3: for x being set st S1[x] holds
H1(x) in ExtREAL ;
consider p being PartFunc of NAT,ExtREAL such that
A4: ( ( for x being set holds
( x in dom p iff ( x in NAT & S1[x] ) ) ) & ( for x being set st x in dom p holds
p . x = H1(x) ) ) from PARTFUN1:sch_3(A3);
for x being set st x in dom F holds
x in dom p by A4;
then A5: dom F c= dom p by TARSKI:def_3;
for x being set st x in dom p holds
x in dom F by A4;
then dom p c= dom F by TARSKI:def_3;
then A6: dom p = dom F by A5, XBOOLE_0:def_10;
then dom p = Seg (len F) by FINSEQ_1:def_3;
then A7: p is FinSequence by FINSEQ_1:def_2;
rng p c= ExtREAL ;
then reconsider p = p as FinSequence of ExtREAL by A7, FINSEQ_1:def_4;
take Sum p ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a, x 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 ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & Sum p = Sum x )
for n being Nat st n in dom p holds
p . n = (a . n) * ((M * F) . n) by A4;
hence ex F being Finite_Sep_Sequence of S ex a, x 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 ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & Sum p = Sum x ) by A2, A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of ExtREAL st ex F being Finite_Sep_Sequence of S ex a, x 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 ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & b1 = Sum x ) & ex F being Finite_Sep_Sequence of S ex a, x 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 ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & b2 = Sum x ) holds
b1 = b2
proof
let s1, s2 be Element of ExtREAL ; ::_thesis: ( ex F being Finite_Sep_Sequence of S ex a, x 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 ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & s1 = Sum x ) & ex F being Finite_Sep_Sequence of S ex a, x 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 ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & s2 = Sum x ) implies s1 = s2 )
assume that
A8: ex F1 being Finite_Sep_Sequence of S ex a1, x1 being FinSequence of ExtREAL st
( F1,a1 are_Re-presentation_of f & a1 . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a1 holds
( 0. < a1 . n & a1 . n < +infty ) ) & dom x1 = dom F1 & ( for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * F1) . n) ) & s1 = Sum x1 ) and
A9: ex F2 being Finite_Sep_Sequence of S ex a2, x2 being FinSequence of ExtREAL st
( F2,a2 are_Re-presentation_of f & a2 . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a2 holds
( 0. < a2 . n & a2 . n < +infty ) ) & dom x2 = dom F2 & ( for n being Nat st n in dom x2 holds
x2 . n = (a2 . n) * ((M * F2) . n) ) & s2 = Sum x2 ) ; ::_thesis: s1 = s2
thus s1 = s2 ::_thesis: verum
proof
consider F2 being Finite_Sep_Sequence of S, a2, x2 being FinSequence of ExtREAL such that
A10: F2,a2 are_Re-presentation_of f and
A11: a2 . 1 = 0. and
A12: for n being Nat st 2 <= n & n in dom a2 holds
( 0. < a2 . n & a2 . n < +infty ) and
A13: dom x2 = dom F2 and
A14: for n being Nat st n in dom x2 holds
x2 . n = (a2 . n) * ((M * F2) . n) and
A15: s2 = Sum x2 by A9;
A16: dom F2 = dom a2 by A10, Def1;
A17: for n being Nat st n in dom a2 holds
0. <= a2 . n
proof
let n be Nat; ::_thesis: ( n in dom a2 implies 0. <= a2 . n )
assume A18: n in dom a2 ; ::_thesis: 0. <= a2 . n
now__::_thesis:_(_(_n_=_1_&_a2_._1_=_0._)_or_(_n_<>_1_&_0._<=_a2_._n_)_)
percases ( n = 1 or n <> 1 ) ;
case n = 1 ; ::_thesis: a2 . 1 = 0.
thus a2 . 1 = 0. by A11; ::_thesis: verum
end;
caseA19: n <> 1 ; ::_thesis: 0. <= a2 . n
n in Seg (len a2) by A18, FINSEQ_1:def_3;
then 1 <= n by FINSEQ_1:1;
then 1 < n by A19, XXREAL_0:1;
then 1 + 1 < n + 1 by XREAL_1:8;
then 2 <= n by NAT_1:13;
hence 0. <= a2 . n by A12, A18; ::_thesis: verum
end;
end;
end;
hence 0. <= a2 . n ; ::_thesis: verum
end;
A20: for n being Nat st n in dom F2 holds
0. <= (M * F2) . n
proof
let n be Nat; ::_thesis: ( n in dom F2 implies 0. <= (M * F2) . n )
assume n in dom F2 ; ::_thesis: 0. <= (M * F2) . n
then ( (M * F2) . n = M . (F2 . n) & F2 . n in rng F2 ) by FUNCT_1:3, FUNCT_1:13;
hence 0. <= (M * F2) . n by SUPINF_2:39; ::_thesis: verum
end;
A21: not -infty in rng x2
proof
assume -infty in rng x2 ; ::_thesis: contradiction
then consider n being set such that
A22: n in dom x2 and
A23: x2 . n = -infty by FUNCT_1:def_3;
( 0. <= a2 . n & 0. <= (M * F2) . n ) by A13, A16, A20, A17, A22;
then 0. <= (a2 . n) * ((M * F2) . n) ;
hence contradiction by A14, A22, A23; ::_thesis: verum
end;
consider F1 being Finite_Sep_Sequence of S, a1, x1 being FinSequence of ExtREAL such that
A23: F1,a1 are_Re-presentation_of f and
A24: a1 . 1 = 0. and
A25: for n being Nat st 2 <= n & n in dom a1 holds
( 0. < a1 . n & a1 . n < +infty ) and
A26: dom x1 = dom F1 and
A27: for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * F1) . n) and
A28: s1 = Sum x1 by A8;
A29: dom F1 = dom a1 by A23, Def1;
A30: for n being Nat st n in dom a1 holds
0. <= a1 . n
proof
let n be Nat; ::_thesis: ( n in dom a1 implies 0. <= a1 . n )
assume A31: n in dom a1 ; ::_thesis: 0. <= a1 . n
now__::_thesis:_(_(_n_=_1_&_a1_._1_=_0._)_or_(_n_<>_1_&_0._<=_a1_._n_)_)
percases ( n = 1 or n <> 1 ) ;
case n = 1 ; ::_thesis: a1 . 1 = 0.
thus a1 . 1 = 0. by A24; ::_thesis: verum
end;
caseA32: n <> 1 ; ::_thesis: 0. <= a1 . n
n in Seg (len a1) by A31, FINSEQ_1:def_3;
then 1 <= n by FINSEQ_1:1;
then 1 < n by A32, XXREAL_0:1;
then 1 + 1 < n + 1 by XREAL_1:8;
then 2 <= n by NAT_1:13;
hence 0. <= a1 . n by A25, A31; ::_thesis: verum
end;
end;
end;
hence 0. <= a1 . n ; ::_thesis: verum
end;
A33: for n being Nat st n in dom F1 holds
0. <= (M * F1) . n
proof
let n be Nat; ::_thesis: ( n in dom F1 implies 0. <= (M * F1) . n )
assume n in dom F1 ; ::_thesis: 0. <= (M * F1) . n
then ( (M * F1) . n = M . (F1 . n) & F1 . n in rng F1 ) by FUNCT_1:3, FUNCT_1:13;
hence 0. <= (M * F1) . n by SUPINF_2:39; ::_thesis: verum
end;
A34: not -infty in rng x1
proof
assume -infty in rng x1 ; ::_thesis: contradiction
then consider n being set such that
A35: n in dom x1 and
A36: x1 . n = -infty by FUNCT_1:def_3;
( 0. <= a1 . n & 0. <= (M * F1) . n ) by A26, A29, A33, A30, A35;
then 0. <= (a1 . n) * ((M * F1) . n) ;
hence contradiction by A27, A35, A36; ::_thesis: verum
end;
now__::_thesis:_(_(_ex_i,_j_being_Nat_st_
(_i_in_dom_F1_&_j_in_dom_F2_&_2_<=_i_&_2_<=_j_&_M_._((F1_._i)_/\_(F2_._j))_=_+infty_)_&_s1_=_s2_)_or_(_(_for_i,_j_being_Nat_st_i_in_dom_F1_&_j_in_dom_F2_&_2_<=_i_&_2_<=_j_holds_
M_._((F1_._i)_/\_(F2_._j))_<>_+infty_)_&_s1_=_s2_)_)
percases ( ex i, j being Nat st
( i in dom F1 & j in dom F2 & 2 <= i & 2 <= j & M . ((F1 . i) /\ (F2 . j)) = +infty ) or for i, j being Nat st i in dom F1 & j in dom F2 & 2 <= i & 2 <= j holds
M . ((F1 . i) /\ (F2 . j)) <> +infty ) ;
case ex i, j being Nat st
( i in dom F1 & j in dom F2 & 2 <= i & 2 <= j & M . ((F1 . i) /\ (F2 . j)) = +infty ) ; ::_thesis: s1 = s2
then consider i, j being Nat such that
A36: i in dom F1 and
A37: j in dom F2 and
A38: 2 <= i and
A39: 2 <= j and
A40: M . ((F1 . i) /\ (F2 . j)) = +infty ;
A41: F2 . j in rng F2 by A37, FUNCT_1:3;
A42: F1 . i in rng F1 by A36, FUNCT_1:3;
then A43: (F1 . i) /\ (F2 . j) in S by A41, MEASURE1:34;
(F1 . i) /\ (F2 . j) c= F1 . i by XBOOLE_1:17;
then M . (F1 . i) = +infty by A40, A42, A43, MEASURE1:31, XXREAL_0:4;
then A44: (M * F1) . i = +infty by A36, FUNCT_1:13;
0. < a1 . i by A25, A29, A36, A38;
then +infty = (a1 . i) * ((M * F1) . i) by A44, XXREAL_3:def_5;
then x1 . i = +infty by A26, A27, A36;
then +infty in rng x1 by A26, A36, FUNCT_1:def_3;
then A45: Sum x1 = +infty by A34, Th17;
(F1 . i) /\ (F2 . j) c= F2 . j by XBOOLE_1:17;
then M . (F2 . j) = +infty by A40, A41, A43, MEASURE1:31, XXREAL_0:4;
then A46: (M * F2) . j = +infty by A37, FUNCT_1:13;
0. < a2 . j by A12, A16, A37, A39;
then +infty = (a2 . j) * ((M * F2) . j) by A46, XXREAL_3:def_5;
then x2 . j = +infty by A13, A14, A37;
then +infty in rng x2 by A13, A37, FUNCT_1:def_3;
hence s1 = s2 by A28, A15, A21, A45, Th17; ::_thesis: verum
end;
caseA47: for i, j being Nat st i in dom F1 & j in dom F2 & 2 <= i & 2 <= j holds
M . ((F1 . i) /\ (F2 . j)) <> +infty ; ::_thesis: s1 = s2
set m = len x2;
set n = len x1;
ex a being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL st
for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds
a . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j)))
proof
deffunc H1( set , set ) -> Element of ExtREAL = (a1 . $1) * (M . ((F1 . $1) /\ (F2 . $2)));
A48: for x, y being set st x in Seg (len x1) & y in Seg (len x2) holds
H1(x,y) in REAL
proof
let x, y be set ; ::_thesis: ( x in Seg (len x1) & y in Seg (len x2) implies H1(x,y) in REAL )
assume that
A49: x in Seg (len x1) and
A50: y in Seg (len x2) ; ::_thesis: H1(x,y) in REAL
x in { k where k is Element of NAT : ( 1 <= k & k <= len x1 ) } by A49, FINSEQ_1:def_1;
then consider kx being Element of NAT such that
A51: x = kx and
A52: 1 <= kx and
kx <= len x1 ;
y in { k where k is Element of NAT : ( 1 <= k & k <= len x2 ) } by A50, FINSEQ_1:def_1;
then consider ky being Element of NAT such that
A53: y = ky and
A54: 1 <= ky and
ky <= len x2 ;
A55: ky in dom F2 by A13, A50, A53, FINSEQ_1:def_3;
then A56: F2 . ky in rng F2 by FUNCT_1:3;
A57: kx in dom F1 by A26, A49, A51, FINSEQ_1:def_3;
then F1 . kx in rng F1 by FUNCT_1:3;
then A58: (F1 . kx) /\ (F2 . ky) in S by A56, MEASURE1:34;
now__::_thesis:_(_(_(_not_2_<=_kx_or_not_2_<=_ky_)_&_H1(kx,ky)_in_REAL_)_or_(_2_<=_kx_&_2_<=_ky_&_H1(kx,ky)_in_REAL_)_)
percases ( not 2 <= kx or not 2 <= ky or ( 2 <= kx & 2 <= ky ) ) ;
caseA59: ( not 2 <= kx or not 2 <= ky ) ; ::_thesis: H1(kx,ky) in REAL
now__::_thesis:_(_(_kx_<_2_&_H1(kx,ky)_in_REAL_)_or_(_ky_<_2_&_H1(kx,ky)_in_REAL_)_)
percases ( kx < 2 or ky < 2 ) by A59;
caseA60: kx < 2 ; ::_thesis: H1(kx,ky) in REAL
then kx <= 1 + 1 ;
then kx <= 1 by A60, NAT_1:8;
then H1(kx,ky) = 0. * (M . ((F1 . kx) /\ (F2 . ky))) by A24, A52, XXREAL_0:1
.= 0 ;
hence H1(kx,ky) in REAL ; ::_thesis: verum
end;
caseA61: ky < 2 ; ::_thesis: H1(kx,ky) in REAL
then ky <= 1 + 1 ;
then A62: ky <= 1 by A61, NAT_1:8;
now__::_thesis:_(_(_(F1_._kx)_/\_(F2_._ky)_=_{}_&_H1(kx,ky)_=_0_)_or_(_(F1_._kx)_/\_(F2_._ky)_<>_{}_&_H1(kx,ky)_=_0_)_)
percases ( (F1 . kx) /\ (F2 . ky) = {} or (F1 . kx) /\ (F2 . ky) <> {} ) ;
case (F1 . kx) /\ (F2 . ky) = {} ; ::_thesis: H1(kx,ky) = 0
hence H1(kx,ky) = (a1 . kx) * 0. by VALUED_0:def_19
.= 0 ;
::_thesis: verum
end;
case (F1 . kx) /\ (F2 . ky) <> {} ; ::_thesis: H1(kx,ky) = 0
then consider x being set such that
A63: x in (F1 . kx) /\ (F2 . ky) by XBOOLE_0:def_1;
A64: x in F2 . ky by A63, XBOOLE_0:def_4;
x in F1 . kx by A63, XBOOLE_0:def_4;
then a1 . kx = f . x by A23, A57, Def1
.= a2 . ky by A10, A55, A64, Def1
.= 0. by A11, A54, A62, XXREAL_0:1 ;
hence H1(kx,ky) = 0 ; ::_thesis: verum
end;
end;
end;
hence H1(kx,ky) in REAL ; ::_thesis: verum
end;
end;
end;
hence H1(kx,ky) in REAL ; ::_thesis: verum
end;
caseA65: ( 2 <= kx & 2 <= ky ) ; ::_thesis: H1(kx,ky) in REAL
A66: 0. <= a1 . kx by A29, A30, A57;
a1 . kx <> +infty by A25, A29, A57, A65;
then reconsider r2 = a1 . kx as Real by A66, XXREAL_0:14;
0. <= M . ((F1 . kx) /\ (F2 . ky)) by A58, SUPINF_2:39;
then reconsider r3 = M . ((F1 . kx) /\ (F2 . ky)) as Real by A47, A57, A55, A65, XXREAL_0:14;
(a1 . kx) * (M . ((F1 . kx) /\ (F2 . ky))) = r2 * r3 by EXTREAL1:1;
hence H1(kx,ky) in REAL ; ::_thesis: verum
end;
end;
end;
hence H1(x,y) in REAL by A51, A53; ::_thesis: verum
end;
consider f being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL such that
A67: for x, y being set st x in Seg (len x1) & y in Seg (len x2) holds
f . (x,y) = H1(x,y) from BINOP_1:sch_2(A48);
take f ; ::_thesis: for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds
f . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j)))
thus for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds
f . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j))) by A67; ::_thesis: verum
end;
then consider a being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL such that
A68: for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds
a . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j))) ;
ex p being FinSequence of REAL st
( dom p = Seg (len x1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) )
proof
defpred S1[ Nat, set ] means ex r being FinSequence of REAL st
( dom r = Seg (len x2) & $2 = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [$1,j] ) );
A69: for k being Nat st k in Seg (len x1) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len x1) implies ex x being set st S1[k,x] )
assume k in Seg (len x1) ; ::_thesis: ex x being set st S1[k,x]
deffunc H1( set ) -> Element of REAL = a . [k,$1];
consider r being FinSequence such that
A70: len r = len x2 and
A71: for i being Nat st i in dom r holds
r . i = H1(i) from FINSEQ_1:sch_2();
A72: dom r = Seg (len x2) by A70, FINSEQ_1:def_3;
for i being Nat st i in dom r holds
r . i in REAL
proof
let i be Nat; ::_thesis: ( i in dom r implies r . i in REAL )
A73: a . [k,i] in REAL ;
assume i in dom r ; ::_thesis: r . i in REAL
hence r . i in REAL by A71, A73; ::_thesis: verum
end;
then reconsider r = r as FinSequence of REAL by FINSEQ_2:12;
take x = Sum r; ::_thesis: S1[k,x]
thus S1[k,x] by A71, A72; ::_thesis: verum
end;
consider p being FinSequence such that
A74: ( dom p = Seg (len x1) & ( for k being Nat st k in Seg (len x1) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_1(A69);
for i being Nat st i in dom p holds
p . i in REAL
proof
let i be Nat; ::_thesis: ( i in dom p implies p . i in REAL )
assume i in dom p ; ::_thesis: p . i in REAL
then ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) by A74;
hence p . i in REAL ; ::_thesis: verum
end;
then reconsider p = p as FinSequence of REAL by FINSEQ_2:12;
take p ; ::_thesis: ( dom p = Seg (len x1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) )
thus ( dom p = Seg (len x1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) ) by A74; ::_thesis: verum
end;
then consider p being FinSequence of REAL such that
A75: dom p = Seg (len x1) and
A76: for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ;
A77: dom p = dom x1 by A75, FINSEQ_1:def_3;
for k being Nat st k in dom p holds
p . k = x1 . k
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k = x1 . k )
assume A78: k in dom p ; ::_thesis: p . k = x1 . k
then consider r being FinSequence of REAL such that
A79: dom r = Seg (len x2) and
A80: p . k = Sum r and
A81: for j being Nat st j in dom r holds
r . j = a . [k,j] by A76;
ex F11 being Finite_Sep_Sequence of S st
( union (rng F11) = F1 . k & dom F11 = dom r & ( for j being Nat st j in dom r holds
F11 . j = (F1 . k) /\ (F2 . j) ) )
proof
deffunc H1( set ) -> set = (F1 . k) /\ (F2 . $1);
consider F being FinSequence such that
A82: len F = len x2 and
A83: for i being Nat st i in dom F holds
F . i = H1(i) from FINSEQ_1:sch_2();
A84: dom F = Seg (len x2) by A82, FINSEQ_1:def_3;
A85: for i being Nat st i in dom F holds
F . i in S
proof
let i be Nat; ::_thesis: ( i in dom F implies F . i in S )
assume A86: i in dom F ; ::_thesis: F . i in S
then i in Seg (len x2) by A82, FINSEQ_1:def_3;
then i in dom F2 by A13, FINSEQ_1:def_3;
then A87: F2 . i in rng F2 by FUNCT_1:3;
F1 . k in rng F1 by A26, A77, A78, FUNCT_1:3;
then (F1 . k) /\ (F2 . i) in S by A87, MEASURE1:34;
hence F . i in S by A83, A86; ::_thesis: verum
end;
A88: dom F = Seg (len x2) by A82, FINSEQ_1:def_3;
reconsider F = F as FinSequence of S by A85, FINSEQ_2:12;
A89: dom F = dom F2 by A13, A88, FINSEQ_1:def_3;
then reconsider F = F as Finite_Sep_Sequence of S by A83, Th5;
take F ; ::_thesis: ( union (rng F) = F1 . k & dom F = dom r & ( for j being Nat st j in dom r holds
F . j = (F1 . k) /\ (F2 . j) ) )
union (rng F) = (F1 . k) /\ (union (rng F2)) by A83, A89, Th6
.= (F1 . k) /\ (dom f) by A10, Def1
.= (F1 . k) /\ (union (rng F1)) by A23, Def1
.= F1 . k by A26, A77, A78, Th7 ;
hence ( union (rng F) = F1 . k & dom F = dom r & ( for j being Nat st j in dom r holds
F . j = (F1 . k) /\ (F2 . j) ) ) by A79, A83, A84; ::_thesis: verum
end;
then consider F11 being Finite_Sep_Sequence of S such that
A90: union (rng F11) = F1 . k and
A91: dom F11 = dom r and
A92: for j being Nat st j in dom r holds
F11 . j = (F1 . k) /\ (F2 . j) ;
A93: Sum (M * F11) = M . (F1 . k) by A90, Th9;
k in Seg (len a1) by A26, A29, A77, A78, FINSEQ_1:def_3;
then A94: 1 <= k by FINSEQ_1:1;
( a1 . k <> -infty & a1 . k <> +infty )
proof
percases ( k = 1 or k <> 1 ) ;
suppose k = 1 ; ::_thesis: ( a1 . k <> -infty & a1 . k <> +infty )
hence ( a1 . k <> -infty & a1 . k <> +infty ) by A24; ::_thesis: verum
end;
suppose k <> 1 ; ::_thesis: ( a1 . k <> -infty & a1 . k <> +infty )
then 1 < k by A94, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
hence ( a1 . k <> -infty & a1 . k <> +infty ) by A25, A26, A29, A77, A78; ::_thesis: verum
end;
end;
end;
then A95: a1 . k is Element of REAL by XXREAL_0:14;
reconsider rr = r as FinSequence of ExtREAL by Th11;
A96: for j being Nat st j in dom r holds
r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j)))
proof
let j be Nat; ::_thesis: ( j in dom r implies r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) )
assume A97: j in dom r ; ::_thesis: r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j)))
hence r . j = a . (k,j) by A81
.= (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) by A68, A75, A78, A79, A97 ;
::_thesis: verum
end;
A98: for j being Nat st j in dom rr holds
rr . j = (a1 . k) * ((M * F11) . j)
proof
let j be Nat; ::_thesis: ( j in dom rr implies rr . j = (a1 . k) * ((M * F11) . j) )
assume A99: j in dom rr ; ::_thesis: rr . j = (a1 . k) * ((M * F11) . j)
hence rr . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) by A96
.= (a1 . k) * (M . (F11 . j)) by A92, A99
.= (a1 . k) * ((M * F11) . j) by A91, A99, FUNCT_1:13 ;
::_thesis: verum
end;
dom rr = dom (M * F11) by A91, Th8;
then Sum rr = (a1 . k) * (Sum (M * F11)) by A98, A95, Th10;
then Sum r = (a1 . k) * (M . (F1 . k)) by A93, Th2
.= (a1 . k) * ((M * F1) . k) by A26, A77, A78, FUNCT_1:13 ;
hence p . k = x1 . k by A27, A77, A78, A80; ::_thesis: verum
end;
then A100: Sum p = Sum x1 by A77, Th2, FINSEQ_1:13;
ex q being FinSequence of REAL st
( dom q = Seg (len x2) & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (len x1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) )
proof
defpred S1[ Nat, set ] means ex s being FinSequence of REAL st
( dom s = Seg (len x1) & $2 = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,$1] ) );
A101: for k being Nat st k in Seg (len x2) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len x2) implies ex x being set st S1[k,x] )
assume k in Seg (len x2) ; ::_thesis: ex x being set st S1[k,x]
deffunc H1( set ) -> Element of REAL = a . [$1,k];
consider s being FinSequence such that
A102: len s = len x1 and
A103: for i being Nat st i in dom s holds
s . i = H1(i) from FINSEQ_1:sch_2();
A104: dom s = Seg (len x1) by A102, FINSEQ_1:def_3;
for i being Nat st i in dom s holds
s . i in REAL
proof
let i be Nat; ::_thesis: ( i in dom s implies s . i in REAL )
A105: a . [i,k] in REAL ;
assume i in dom s ; ::_thesis: s . i in REAL
hence s . i in REAL by A103, A105; ::_thesis: verum
end;
then reconsider s = s as FinSequence of REAL by FINSEQ_2:12;
take x = Sum s; ::_thesis: S1[k,x]
thus S1[k,x] by A103, A104; ::_thesis: verum
end;
consider p being FinSequence such that
A106: ( dom p = Seg (len x2) & ( for k being Nat st k in Seg (len x2) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_1(A101);
for i being Nat st i in dom p holds
p . i in REAL
proof
let i be Nat; ::_thesis: ( i in dom p implies p . i in REAL )
assume i in dom p ; ::_thesis: p . i in REAL
then ex s being FinSequence of REAL st
( dom s = Seg (len x1) & p . i = Sum s & ( for j being Nat st j in dom s holds
s . j = a . [j,i] ) ) by A106;
hence p . i in REAL ; ::_thesis: verum
end;
then reconsider p = p as FinSequence of REAL by FINSEQ_2:12;
take p ; ::_thesis: ( dom p = Seg (len x2) & ( for j being Nat st j in dom p holds
ex s being FinSequence of REAL st
( dom s = Seg (len x1) & p . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) )
thus ( dom p = Seg (len x2) & ( for j being Nat st j in dom p holds
ex s being FinSequence of REAL st
( dom s = Seg (len x1) & p . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) ) by A106; ::_thesis: verum
end;
then consider q being FinSequence of REAL such that
A107: dom q = Seg (len x2) and
A108: for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (len x1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ;
A109: dom q = dom x2 by A107, FINSEQ_1:def_3;
A110: for k being Nat st k in dom q holds
q . k = x2 . k
proof
let k be Nat; ::_thesis: ( k in dom q implies q . k = x2 . k )
assume A111: k in dom q ; ::_thesis: q . k = x2 . k
then consider s being FinSequence of REAL such that
A112: dom s = Seg (len x1) and
A113: q . k = Sum s and
A114: for i being Nat st i in dom s holds
s . i = a . [i,k] by A108;
reconsider ss = s as FinSequence of ExtREAL by Th11;
ex F21 being Finite_Sep_Sequence of S st
( union (rng F21) = F2 . k & dom F21 = dom s & ( for j being Nat st j in dom s holds
F21 . j = (F1 . j) /\ (F2 . k) ) )
proof
deffunc H1( set ) -> set = (F2 . k) /\ (F1 . $1);
consider F being FinSequence such that
A115: len F = len x1 and
A116: for i being Nat st i in dom F holds
F . i = H1(i) from FINSEQ_1:sch_2();
A117: dom F = Seg (len x1) by A115, FINSEQ_1:def_3;
A118: for i being Nat st i in dom F holds
F . i in S
proof
let i be Nat; ::_thesis: ( i in dom F implies F . i in S )
assume A119: i in dom F ; ::_thesis: F . i in S
then i in Seg (len x1) by A115, FINSEQ_1:def_3;
then i in dom F1 by A26, FINSEQ_1:def_3;
then A120: F1 . i in rng F1 by FUNCT_1:3;
F2 . k in rng F2 by A13, A109, A111, FUNCT_1:3;
then (F1 . i) /\ (F2 . k) in S by A120, MEASURE1:34;
hence F . i in S by A116, A119; ::_thesis: verum
end;
A121: dom F = Seg (len x1) by A115, FINSEQ_1:def_3;
reconsider F = F as FinSequence of S by A118, FINSEQ_2:12;
A122: dom F = dom F1 by A26, A121, FINSEQ_1:def_3;
then reconsider F = F as Finite_Sep_Sequence of S by A116, Th5;
take F ; ::_thesis: ( union (rng F) = F2 . k & dom F = dom s & ( for j being Nat st j in dom s holds
F . j = (F1 . j) /\ (F2 . k) ) )
union (rng F) = (F2 . k) /\ (union (rng F1)) by A116, A122, Th6
.= (F2 . k) /\ (dom f) by A23, Def1
.= (F2 . k) /\ (union (rng F2)) by A10, Def1
.= F2 . k by A13, A109, A111, Th7 ;
hence ( union (rng F) = F2 . k & dom F = dom s & ( for j being Nat st j in dom s holds
F . j = (F1 . j) /\ (F2 . k) ) ) by A112, A116, A117; ::_thesis: verum
end;
then consider F21 being Finite_Sep_Sequence of S such that
A123: union (rng F21) = F2 . k and
A124: dom F21 = dom s and
A125: for i being Nat st i in dom s holds
F21 . i = (F1 . i) /\ (F2 . k) ;
A126: Sum (M * F21) = M . (F2 . k) by A123, Th9;
A127: for i being Nat st i in dom s holds
s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k)))
proof
let i be Nat; ::_thesis: ( i in dom s implies s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k))) )
assume A128: i in dom s ; ::_thesis: s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k)))
hence s . i = a . (i,k) by A114
.= (a1 . i) * (M . ((F1 . i) /\ (F2 . k))) by A68, A107, A111, A112, A128 ;
::_thesis: verum
end;
A129: for i being Nat st i in dom s holds
s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k)))
proof
let i be Nat; ::_thesis: ( i in dom s implies s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) )
assume A130: i in dom s ; ::_thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k)))
now__::_thesis:_(_(_(F1_._i)_/\_(F2_._k)_=_{}_&_s_._i_=_(a2_._k)_*_(M_._((F1_._i)_/\_(F2_._k)))_)_or_(_(F1_._i)_/\_(F2_._k)_<>_{}_&_s_._i_=_(a2_._k)_*_(M_._((F1_._i)_/\_(F2_._k)))_)_)
percases ( (F1 . i) /\ (F2 . k) = {} or (F1 . i) /\ (F2 . k) <> {} ) ;
caseA131: (F1 . i) /\ (F2 . k) = {} ; ::_thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k)))
then M . ((F1 . i) /\ (F2 . k)) = 0. by VALUED_0:def_19;
hence s . i = (a1 . i) * 0. by A127, A130
.= 0.
.= (a2 . k) * 0.
.= (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) by A131, VALUED_0:def_19 ;
::_thesis: verum
end;
case (F1 . i) /\ (F2 . k) <> {} ; ::_thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k)))
then consider x being set such that
A132: x in (F1 . i) /\ (F2 . k) by XBOOLE_0:def_1;
A133: x in F2 . k by A132, XBOOLE_0:def_4;
A134: dom p = dom x1 by A75, FINSEQ_1:def_3;
x in F1 . i by A132, XBOOLE_0:def_4;
then a1 . i = f . x by A23, A26, A75, A112, A130, A134, Def1
.= a2 . k by A10, A13, A109, A111, A133, Def1 ;
hence s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) by A127, A130; ::_thesis: verum
end;
end;
end;
hence s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) ; ::_thesis: verum
end;
A135: for j being Nat st j in dom ss holds
ss . j = (a2 . k) * ((M * F21) . j)
proof
let j be Nat; ::_thesis: ( j in dom ss implies ss . j = (a2 . k) * ((M * F21) . j) )
assume A136: j in dom ss ; ::_thesis: ss . j = (a2 . k) * ((M * F21) . j)
hence ss . j = (a2 . k) * (M . ((F1 . j) /\ (F2 . k))) by A129
.= (a2 . k) * (M . (F21 . j)) by A125, A136
.= (a2 . k) * ((M * F21) . j) by A124, A136, FUNCT_1:13 ;
::_thesis: verum
end;
k in Seg (len a2) by A13, A16, A109, A111, FINSEQ_1:def_3;
then A137: 1 <= k by FINSEQ_1:1;
( a2 . k <> -infty & a2 . k <> +infty )
proof
percases ( k = 1 or k <> 1 ) ;
suppose k = 1 ; ::_thesis: ( a2 . k <> -infty & a2 . k <> +infty )
hence ( a2 . k <> -infty & a2 . k <> +infty ) by A11; ::_thesis: verum
end;
suppose k <> 1 ; ::_thesis: ( a2 . k <> -infty & a2 . k <> +infty )
then 1 < k by A137, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
hence ( a2 . k <> -infty & a2 . k <> +infty ) by A12, A13, A16, A109, A111; ::_thesis: verum
end;
end;
end;
then A138: a2 . k is Element of REAL by XXREAL_0:14;
dom ss = dom (M * F21) by A124, Th8;
then Sum ss = (a2 . k) * (Sum (M * F21)) by A135, A138, Th10;
then Sum s = (a2 . k) * (M . (F2 . k)) by A126, Th2
.= (a2 . k) * ((M * F2) . k) by A13, A109, A111, FUNCT_1:13 ;
hence q . k = x2 . k by A14, A109, A111, A113; ::_thesis: verum
end;
Sum p = Sum q by A75, A76, A107, A108, Th1;
hence s1 = s2 by A28, A15, A100, A109, A110, Th2, FINSEQ_1:13; ::_thesis: verum
end;
end;
end;
hence s1 = s2 ; ::_thesis: verum
end;
end;
end;
:: deftheorem defines integral MESFUNC3:def_2_:_
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds
0. <= f . x ) holds
for b5 being Element of ExtREAL holds
( b5 = integral (X,S,M,f) iff ex F being Finite_Sep_Sequence of S ex a, x 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 ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & b5 = Sum x ) );
begin
theorem :: MESFUNC3:18
for a being FinSequence of ExtREAL
for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds
a . n = p ) holds
Sum a = N * p by Lm1;