let a, b be Real; :: thesis: for A being non empty closed_interval Subset of REAL
for D being Division of A
for f being PartFunc of A,REAL st A = [.a,b.] holds
ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for f being PartFunc of A,REAL st A = [.a,b.] holds
ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

let D be Division of A; :: thesis: for f being PartFunc of A,REAL st A = [.a,b.] holds
ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

let f be PartFunc of A,REAL; :: thesis: ( A = [.a,b.] implies ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) ) )

assume A = [.a,b.] ; :: thesis: ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

then consider F being Finite_Sep_Sequence of Borel_Sets such that
A1: dom F = dom D and
A2: union (rng F) = A and
A3: for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) by Th9;
defpred S1[ object , object ] means ex k being Nat st
( 1 <= k & k <= len F & \$1 in F . k & \$2 = upper_bound (rng (f | (divset (D,k)))) );
A4: for x, y being object st x in REAL & S1[x,y] holds
y in ExtREAL by XXREAL_0:def 1;
A5: for x, y1, y2 being object st x in REAL & S1[x,y1] & S1[x,y2] holds
y1 = y2 by ;
consider g being PartFunc of REAL,ExtREAL such that
A6: for x being object holds
( x in dom g iff ( x in REAL & ex y being object st S1[x,y] ) ) and
A7: for x being object st x in dom g holds
S1[x,g . x] from
now :: thesis: for y being object st y in rng g holds
y in REAL
let y be object ; :: thesis: ( y in rng g implies y in REAL )
assume y in rng g ; :: thesis:
then consider x being Element of REAL such that
A8: ( x in dom g & y = g . x ) by PARTFUN1:3;
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) by A7, A8;
hence y in REAL by ; :: thesis: verum
end;
then rng g c= REAL ;
then A9: g is V55() by VALUED_0:def 3;
now :: thesis: for x being object st x in dom g holds
x in union (rng F)
let x be object ; :: thesis: ( x in dom g implies x in union (rng F) )
assume x in dom g ; :: thesis: x in union (rng F)
then consider y being object such that
A10: ex k being Nat st
( 1 <= k & k <= len F & x in F . k & y = upper_bound (rng (f | (divset (D,k)))) ) by A6;
consider k being Nat such that
A11: ( 1 <= k & k <= len F ) and
A12: x in F . k and
y = upper_bound (rng (f | (divset (D,k)))) by A10;
k in dom F by ;
then F . k in rng F by FUNCT_1:3;
hence x in union (rng F) by ; :: thesis: verum
end;
then A13: dom g c= union (rng F) ;
now :: thesis: for x being object st x in union (rng F) holds
x in dom g
let x be object ; :: thesis: ( x in union (rng F) implies x in dom g )
assume A14: x in union (rng F) ; :: thesis: x in dom g
then consider P being set such that
A15: ( x in P & P in rng F ) by TARSKI:def 4;
consider k being Element of NAT such that
A16: ( k in dom F & P = F . k ) by ;
A17: ( 1 <= k & k <= len F ) by ;
upper_bound (rng (f | (divset (D,k)))) in REAL by XREAL_0:def 1;
hence x in dom g by A6, A14, A2, A15, A16, A17; :: thesis: verum
end;
then union (rng F) c= dom g ;
then A18: dom g = union (rng F) by ;
A19: for k being Nat
for x, y being Element of REAL st k in dom F & x in F . k & y in F . k holds
g . x = g . y
proof
let k be Nat; :: thesis: for x, y being Element of REAL st k in dom F & x in F . k & y in F . k holds
g . x = g . y

let x, y be Element of REAL ; :: thesis: ( k in dom F & x in F . k & y in F . k implies g . x = g . y )
assume that
A20: k in dom F and
A21: x in F . k and
A22: y in F . k ; :: thesis: g . x = g . y
F . k in rng F by ;
then A23: ( x in dom g & y in dom g ) by ;
then consider k1 being Nat such that
( 1 <= k1 & k1 <= len F ) and
A24: x in F . k1 and
A25: g . x = upper_bound (rng (f | (divset (D,k1)))) by A7;
consider k2 being Nat such that
( 1 <= k2 & k2 <= len F ) and
A26: y in F . k2 and
A27: g . y = upper_bound (rng (f | (divset (D,k2)))) by ;
( k = k1 & k = k2 ) by ;
hence g . x = g . y by ; :: thesis: verum
end;
for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) by A7;
hence ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) ) by ; :: thesis: verum