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 & f is nonnegative & ( for x being object 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 & f is nonnegative & ( for x being object 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 & f is nonnegative & ( for x being object 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: f is nonnegative and
A3: for x being object 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 ) ) )
a2: for x being object st x in dom f holds
0. <= f . x by A2, SUPINF_2:39;
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 object st x <> y holds
F . x misses F . y

proof

let x, y be object ; :: 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 ) )

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 ;
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 ) )

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

case A16: ( 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 ) )

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

case A18: 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;
hence F . x misses F . y ; :: thesis: verum

end;

case A19: 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;
hence F . x misses F . y ; :: thesis: verum

end;

end;

end;

hence F . x misses F . y ; :: thesis: verum

end;

case A20: ( 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 ; :: 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 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 ) );
A24: 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 A25: 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

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

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

take y = 0. ; :: thesis: S₁[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 S₁[k,y] ; :: thesis: verum

end;

suppose A27: k <> 1 ; :: thesis: ex y being Element of ExtREAL st S₁[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 object such that
A36: z in F . k by XBOOLE_0:def 1;
reconsider z = z as set by TARSKI:1;
take y = f . z; :: thesis: S₁[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 S₁[k,y] by A37; :: thesis: verum

end;

end;

end;

hence ex y being Element of ExtREAL st S₁[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
S₁[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 object 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 real-valued 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 A23, A51, A52, A54, A53, EXTREAL1:21, a2; :: 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 object st x in F . n9 holds
f . x = a . n9

proof

let n9 be Nat; :: thesis: ( n9 in dom F implies for x being object st x in F . n9 holds
f . x = a . n9 )
assume A56: n9 in dom F ; :: thesis: for x being object 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 ) ) )

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

case A57: 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
.= {} ;
assume x in F . n9 ; :: thesis: f . x = a . n9
hence f . x = a . n9 by A57, A58; :: thesis: verum

end;

end;

case A59: 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 object 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; :: thesis: verum