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 5;
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:55, MEASURE1:21;
then ( rng <*{} *> c= S & rng G c= S ) by ZFMISC_1:37;
then (rng <*{} *>) \/ (rng G) c= S by XBOOLE_1:8;
then rng (<*{} *> ^ G) c= S by FINSEQ_1:44;
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

per cases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ;

case A9: ( x in dom F & y in dom F ) ; :: thesis: F . x misses F . y

then reconsider x = x, y = y as Element of NAT ;
( x in Seg (len (<*{} *> ^ G)) & y in Seg (len (<*{} *> ^ G)) ) by A9, FINSEQ_1:def 3;
then A10: ( 1 <= x & x <= len (<*{} *> ^ G) & 1 <= y & y <= len (<*{} *> ^ G) ) by FINSEQ_1:3;

now

per cases ( x = 1 or y = 1 or ( x <> 1 & y <> 1 ) ) ;

case A11: ( x = 1 or y = 1 ) ; :: thesis: F . x misses F . y

A12: dom <*{} *> = Seg 1 by FINSEQ_1:55;

now

per cases ( x = 1 or y = 1 ) by A11;

case A13: x = 1 ; :: thesis: F . x misses F . y

then x in dom <*{} *> by A12, FINSEQ_1:4, TARSKI:def 1;
then F . x = <*{} *> . x by FINSEQ_1:def 7;
then F . x = {} by A13, FINSEQ_1:def 8;
hence F . x misses F . y by XBOOLE_1:65; :: thesis: verum

end;

case A14: y = 1 ; :: thesis: F . x misses F . y

then y in dom <*{} *> by A12, FINSEQ_1:4, TARSKI:def 1;
then F . y = <*{} *> . y by FINSEQ_1:def 7;
then F . y = {} by A14, 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;

case ( x <> 1 & y <> 1 ) ; :: thesis: F . x misses F . y

then ( 1 < x & 1 < y ) by A10, XXREAL_0:1;
then ( len <*{} *> < x & len <*{} *> < y ) by FINSEQ_1:57;
then A15: ( F . x = G . (x - (len <*{} *>)) & F . y = G . (y - (len <*{} *>)) ) by A10, FINSEQ_1:37;
x - (len <*{} *>) <> y - (len <*{} *>) by A8;
hence F . x misses F . y by A15, PROB_2:def 3; :: 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 4;
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 3;
A16: union (rng F) = union ((rng <*{} *>) \/ (rng G)) by FINSEQ_1:44
.= union ({{} } \/ (rng G)) by FINSEQ_1:55
.= (union {{} }) \/ (union (rng G)) by ZFMISC_1:96
.= {} \/ (union (rng G)) by ZFMISC_1:31
.= dom f by A4, A6 ;
defpred S₁[ 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 ) );
A17: for k being Nat st k in Seg (len F) holds
ex y being Element of ExtREAL st S₁[k,y]

proof

let k be Nat; :: thesis: ( k in Seg (len F) implies ex y being Element of ExtREAL st S₁[k,y] )
assume A18: k in Seg (len F) ; :: thesis: ex y being Element of ExtREAL st S₁[k,y]
ex y being Element of ExtREAL st S₁[k,y]

proof

now

per cases ( k = 1 or k <> 1 ) ;

case A19: k = 1 ; :: thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S₁[k,y]

take y = 0. ; :: thesis: ex y being Element of ExtREAL st S₁[k,y]
A20: 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 A19;
hence ex y being Element of ExtREAL st S₁[k,y] by A20; :: thesis: verum

end;

case A21: k <> 1 ; :: thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S₁[k,y]

( 1 <= k & k <= len F ) by A18, FINSEQ_1:3;
then A22: ( 1 < k & k <= (len <*{} *>) + (len G) ) by A21, FINSEQ_1:35, XXREAL_0:1;
then ( 1 + 1 <= k & k <= (len <*{} *>) + (len G) ) by NAT_1:13;
then A23: ( (len <*{} *>) + 1 <= k & k <= (len <*{} *>) + (len G) ) by FINSEQ_1:56;
then consider k2 being Nat such that
A24: ((len <*{} *>) + 1) + k2 = k by NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 13;
1 + k2 = k - (len <*{} *>) by A24;
then A25: 1 <= 1 + k2 by A23, XREAL_1:21;
k - (len <*{} *>) <= len G by A22, XREAL_1:22;
then 1 + k2 in Seg (len G) by A24, A25, FINSEQ_1:3;
then A26: 1 + k2 in dom G by FINSEQ_1:def 3;
A27: F . k = G . (k - (len <*{} *>)) by A23, FINSEQ_1:36
.= G . (1 + k2) by A24 ;
then F . k <> {} by A7, A26;
then consider z being set such that
A28: z in F . k by XBOOLE_0:def 1;
take y = f . z; :: thesis: ex y being Element of ExtREAL st S₁[k,y]
consider m1 being Nat such that
A29: ( m1 in dom F1 & F1 . m1 = G . (1 + k2) ) by A7, A26;
( F . k in rng F1 & rng F1 c= S ) by A27, A29, FUNCT_1:12;
then ( F . k in S & S c= bool X ) ;
then reconsider z = z as Element of X by A28;
A30: for x being Element of X st k in dom F & k = 1 holds
y = 0. by A21;
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 ( k in dom F & k >= 2 & x in F . k ) ; :: thesis: y = f . x
then ( z in F1 . m1 & x in F1 . m1 ) by A27, A28, A29;
hence y = f . x by A5, A29; :: thesis: verum

end;

hence ex y being Element of ExtREAL st S₁[k,y] by A30; :: thesis: verum

end;

end;

end;

hence ex y being Element of ExtREAL st S₁[k,y] ; :: thesis: verum

end;

hence ex y being Element of ExtREAL st S₁[k,y] ; :: thesis: verum

end;

consider a being FinSequence of ExtREAL such that
A31: ( dom a = Seg (len F) & ( for n being Nat st n in Seg (len F) holds
S₁[n,a . n] ) ) from FINSEQ_1:sch 5(A17);
A32: ( dom F = dom a & a . 1 = 0. & ( 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

thus dom a = dom F by A31, FINSEQ_1:def 3; :: thesis: ( a . 1 = 0. & ( 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 ) )
len F = (len <*{} *>) + (len G) by FINSEQ_1:35
.= 1 + (len G) by FINSEQ_1:56 ;
then 1 <= len F by NAT_1:11;
then A33: 1 in Seg (len F) by FINSEQ_1:3;
then 1 in dom F by FINSEQ_1:def 3;
hence a . 1 = 0. by A31, A33; :: thesis: 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
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 A34: ( n in dom F & n >= 2 & x in F . n ) ; :: thesis: a . n = f . x
then n in Seg (len F) by FINSEQ_1:def 3;
hence a . n = f . x by A31, A34; :: thesis: verum

end;

hence 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 ; :: thesis: verum

end;

A35: 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 A36: n' in dom F ; :: thesis: for x being set st x in F . n' holds
f . x = a . n'

now

per cases ( n' = 1 or n' <> 1 ) ;

case A37: n' = 1 ; :: thesis: for x being set st x in F . n' holds
f . x = a . n'

thus for x being set st x in F . n' holds
f . x = a . n' :: thesis: verum

proof

let x be set ; :: thesis: ( x in F . n' implies f . x = a . n' )
assume A38: x in F . n' ; :: thesis: f . x = a . n'
dom <*{} *> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then 1 in dom <*{} *> by TARSKI:def 1;
then F . 1 = <*{} *> . 1 by FINSEQ_1:def 7
.= {} by FINSEQ_1:57 ;
hence f . x = a . n' by A37, A38; :: thesis: verum

end;

end;

case A39: n' <> 1 ; :: thesis: for x being set st x in F . n' holds
f . x = a . n'

n' in Seg (len F) by A36, FINSEQ_1:def 3;
then ( 1 <= n' & n' <= len F ) by FINSEQ_1:3;
then 1 < n' by A39, XXREAL_0:1;
then A40: 1 + 1 <= n' by NAT_1:13;
thus for x being set st x in F . n' holds
f . x = a . n' :: thesis: verum

proof

let x be set ; :: thesis: ( x in F . n' implies f . x = a . n' )
assume A41: x in F . n' ; :: thesis: f . x = a . n'
( F . n' in rng F & rng F c= S ) by A36, FUNCT_1:12;
then ( F . n' in S & S c= bool X ) ;
then reconsider x = x as Element of X by A41;
a . n' = f . x by A32, A36, A40, A41;
hence f . x = a . n' ; :: thesis: verum

end;

end;

end;

end;

hence for x being set st x in F . n' holds
f . x = a . n' ; :: thesis: verum

end;

A42: 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
A43: 2 <= n and
A44: n in dom a ; :: thesis: ( 0. < a . n & a . n < +infty )
n in Seg (len F) by A32, A44, FINSEQ_1:def 3;
then n <= len F by FINSEQ_1:3;
then A45: n <= (len <*{} *>) + (len G) by FINSEQ_1:35;
1 + 1 <= n by A43;
then (len <*{} *>) + 1 <= n by FINSEQ_1:56;
then A46: F . n = G . (n - (len <*{} *>)) by A45, FINSEQ_1:36
.= G . (n - 1) by FINSEQ_1:56 ;
A47: dom <*{} *> = {1} by FINSEQ_1:4, FINSEQ_1:55;
1 <> n by A43;
then not n in dom <*{} *> by A47, TARSKI:def 1;
then consider k being Nat such that
A48: ( k in dom G & n = (len <*{} *>) + k ) by A32, A44, FINSEQ_1:38;
n = 1 + k by A48, FINSEQ_1:56;
then F . n <> {} by A7, A46, A48;
then consider x1 being set such that
A49: x1 in F . n by XBOOLE_0:def 1;
A50: F . n c= union (rng F) by A32, A44, FUNCT_1:12, ZFMISC_1:92;
then ( x1 in dom f & dom f c= X ) by A16, A49;
then reconsider x1 = x1 as Element of X ;
A51: a . n = f . x1 by A32, A43, A44, A49;
f is real-valued by A1, MESFUNC2:def 5;
then A52: |.(f . x1).| < +infty by A16, A49, A50, MESFUNC2:def 1;
( 0. <= f . x1 & 0. <> f . x1 ) by A2, A3, A16, A49, A50;
hence ( 0. < a . n & a . n < +infty ) by A51, A52, EXTREAL2:58; :: 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 ) ) )
thus ( 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 A16, A32, A35, A42, Def1; :: thesis: verum