let a, b be Real; :: thesis: for A being non empty closed_interval Subset of REAL
for D being Division of A st A = [.a,b.] holds
ex F being Finite_Sep_Sequence of Borel_Sets st
( dom D = dom F & 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).] ) ) ) ) ) )
let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st A = [.a,b.] holds
ex F being Finite_Sep_Sequence of Borel_Sets st
( dom D = dom F & 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).] ) ) ) ) ) )
let D be Division of A; :: thesis: ( A = [.a,b.] implies ex F being Finite_Sep_Sequence of Borel_Sets st
( dom D = dom F & 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).] ) ) ) ) ) ) )
assume A1: A = [.a,b.] ; :: thesis: ex F being Finite_Sep_Sequence of Borel_Sets st
( dom D = dom F & 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).] ) ) ) ) ) )
defpred S₁[ Nat, set ] means ( ( len D = 1 implies $2 = [.a,b.] ) & ( len D <> 1 implies ( ( $1 = 1 implies $2 = [.a,(D . $1).[ ) & ( 1 < $1 & $1 < len D implies $2 = [.(D . ($1 -' 1)),(D . $1).[ ) & ( $1 = len D implies $2 = [.(D . ($1 -' 1)),(D . $1).] ) ) ) );
A2: for k being Nat st k in Seg (len D) holds
ex x being Element of Borel_Sets st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len D) implies ex x being Element of Borel_Sets st S₁[k,x] )
assume k in Seg (len D) ; :: thesis: ex x being Element of Borel_Sets st S₁[k,x]
then ( 1 <= k & k <= len D ) by FINSEQ_1:1;
then A3: ( ( k = 1 & k <> len D ) or ( 1 < k & k < len D ) or k = len D ) by XXREAL_0:1;
A4: ( [.a,b.] is Element of Borel_Sets & [.a,(D . k).[ is Element of Borel_Sets & [.(D . (k -' 1)),(D . k).[ is Element of Borel_Sets & [.(D . (k -' 1)),(D . k).] is Element of Borel_Sets ) by MEASUR10:5;
( len D = 1 or len D <> 1 ) ;
hence ex x being Element of Borel_Sets st S₁[k,x] by A3, A4; :: thesis: verum

end;

consider F being FinSequence of Borel_Sets such that
A5: ( dom F = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S₁[k,F . k] ) ) from FINSEQ_1:sch 5(A2);
A6: dom F = dom D by A5, FINSEQ_1:def 3;
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 A7: x <> y ; :: thesis: F . x misses F . y

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

suppose ( 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;

suppose A8: ( x in dom F & y in dom F ) ; :: thesis: F . x misses F . y

then reconsider x1 = x, y1 = y as Nat ;
A9: ( x in dom D & y in dom D ) by A8, A5, FINSEQ_1:def 3;
A10: ( 1 <= x1 & x1 <= len D & 1 <= y1 & y1 <= len D ) by A8, A5, FINSEQ_1:1;

A11: now :: thesis: not len D = 1

assume len D = 1 ; :: thesis: contradiction
then ( x1 = 1 & y1 = 1 ) by A10, XXREAL_0:1;
hence contradiction by A7; :: thesis: verum

end;

per cases ( 1 = x1 or ( 1 < x1 & x1 < len D ) or x1 = len D ) by A10, XXREAL_0:1;

suppose A12: 1 = x1 ; :: thesis: F . x misses F . y

then A13: ( 1 < y1 & y1 <= len D ) by A7, A10, XXREAL_0:1;
then A14: ( x1 <= y1 -' 1 & y1 -' 1 <= len D ) by A12, NAT_D:44, NAT_D:49;
then A15: y1 -' 1 in dom D by A12, FINSEQ_3:25;
A16: F . x = [.a,(D . x1).[ by A8, A5, A12, A11;
( y1 < len D or y1 = len D ) by A10, XXREAL_0:1;
then ( F . y = [.(D . (y1 -' 1)),(D . y1).[ or F . y = [.(D . (y1 -' 1)),(D . y1).] ) by A8, A5, A13;
hence F . x misses F . y by A16, A14, A9, A15, VALUED_0:def 15, XXREAL_1:95, XXREAL_1:96; :: thesis: verum

end;

suppose A17: ( 1 < x1 & x1 < len D ) ; :: thesis: F . x misses F . y

then x1 in Seg (len D) by FINSEQ_1:1;
then A18: F . x = [.(D . (x1 -' 1)),(D . x1).[ by A5, A17;

per cases ( x1 < y1 or x1 > y1 ) by A7, XXREAL_0:1;

suppose A19: x1 < y1 ; :: thesis: F . x misses F . y

then A20: x1 <= y1 -' 1 by NAT_D:49;
then ( 1 <= y1 -' 1 & y1 -' 1 <= len D ) by A10, NAT_D:44, XXREAL_0:2;
then A21: y1 -' 1 in dom D by FINSEQ_3:25;
( y1 = len D or ( 1 < y1 & y1 < len D ) ) by A19, A10, XXREAL_0:1;
then ( F . y = [.(D . (y1 -' 1)),(D . y1).] or F . y = [.(D . (y1 -' 1)),(D . y1).[ ) by A8, A11, A5;
hence F . x misses F . y by A21, A18, A9, A20, VALUED_0:def 15, XXREAL_1:95, XXREAL_1:96; :: thesis: verum

end;

suppose A22: x1 > y1 ; :: thesis: F . x misses F . y

then A23: y1 <= x1 -' 1 by NAT_D:49;
then ( 1 <= x1 -' 1 & x1 -' 1 <= len D ) by A10, XXREAL_0:2, NAT_D:44;
then A24: x1 -' 1 in dom D by FINSEQ_3:25;
( y1 = 1 or ( 1 < y1 & y1 < len D ) ) by A10, A22, XXREAL_0:1;
then ( F . y = [.a,(D . y1).[ or F . y = [.(D . (y1 -' 1)),(D . y1).[ ) by A5, A8, A11;
hence F . x misses F . y by A18, A24, A9, A23, VALUED_0:def 15, XXREAL_1:96; :: thesis: verum

end;

end;

end;

suppose A25: x1 = len D ; :: thesis: F . x misses F . y

then A26: F . x = [.(D . (x1 -' 1)),(D . x1).] by A5, A8, A11;
A27: y1 < len D by A7, A10, A25, XXREAL_0:1;
then A28: y1 <= x1 -' 1 by A25, NAT_D:49;
then ( 1 <= x1 -' 1 & x1 -' 1 <= len D ) by A10, XXREAL_0:2, NAT_D:44;
then A29: x1 -' 1 in dom D by FINSEQ_3:25;
( y1 = 1 or 1 < y1 ) by A10, XXREAL_0:1;
then ( F . y = [.a,(D . y1).[ or F . y = [.(D . (y1 -' 1)),(D . y1).[ ) by A5, A8, A27;
hence F . x misses F . y by A26, A29, A9, A28, VALUED_0:def 15, XXREAL_1:95; :: thesis: verum

end;

end;

end;

end;

end;

then reconsider F = F as Finite_Sep_Sequence of Borel_Sets by PROB_2:def 2;
take F ; :: thesis: ( dom D = dom F & 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).] ) ) ) ) ) )
A30: for k being Nat st k in dom F & k <> len D holds
union (rng (F | k)) = [.a,(D . k).[

proof

let k be Nat; :: thesis: ( k in dom F & k <> len D implies union (rng (F | k)) = [.a,(D . k).[ )
assume that
A31: k in dom F and
A32: k <> len D ; :: thesis: union (rng (F | k)) = [.a,(D . k).[
A33: k <= len F by A31, FINSEQ_3:25;
len D = len F by A5, FINSEQ_1:def 3;
then A34: k < len D by A32, A33, XXREAL_0:1;
defpred S₂[ Nat] means ( 1 <= $1 & $1 <= k implies union (rng (F | $1)) = [.a,(D . $1).[ );
A35: S₂[ 0 ] ;
A36: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A37: S₂[i] ; :: thesis: S₂[i + 1]
assume A38: ( 1 <= i + 1 & i + 1 <= k ) ; :: thesis: union (rng (F | (i + 1))) = [.a,(D . (i + 1)).[
then A39: i + 1 < len D by A34, XXREAL_0:2;
i + 1 <= len F by A38, A33, XXREAL_0:2;
then A40: i + 1 in dom F by A38, FINSEQ_3:25;

per cases ( i = 0 or i <> 0 ) ;

suppose A41: i = 0 ; :: thesis: union (rng (F | (i + 1))) = [.a,(D . (i + 1)).[

then len (F | (i + 1)) = 1 by A38, A33, XXREAL_0:2, FINSEQ_1:59;
then F | (i + 1) = <*((F | (i + 1)) . 1)*> by FINSEQ_1:40;
then F | (i + 1) = <*(F . 1)*> by A41, FINSEQ_3:112;
then rng (F | (i + 1)) = {(F . 1)} by FINSEQ_1:38;
hence union (rng (F | (i + 1))) = [.a,(D . (i + 1)).[ by A5, A40, A41, A38, A34; :: thesis: verum

end;

suppose A42: i <> 0 ; :: thesis: union (rng (F | (i + 1))) = [.a,(D . (i + 1)).[

then A43: i >= 1 by NAT_1:14;
A44: i < i + 1 by NAT_1:13;
then (F | (i + 1)) | i = F | i by FINSEQ_1:82;
then A45: F | i = (F | (i + 1)) | (Seg i) by FINSEQ_1:def 16;
len (F | (i + 1)) = i + 1 by A38, A33, XXREAL_0:2, FINSEQ_1:59;
then F | (i + 1) = (F | i) ^ <*((F | (i + 1)) . (i + 1))*> by A45, FINSEQ_3:55;
then F | (i + 1) = (F | i) ^ <*(F . (i + 1))*> by FINSEQ_3:112;
then rng (F | (i + 1)) = (rng (F | i)) \/ (rng <*(F . (i + 1))*>) by FINSEQ_1:31;
then rng (F | (i + 1)) = (rng (F | i)) \/ {(F . (i + 1))} by FINSEQ_1:38;
then A46: union (rng (F | (i + 1))) = (union (rng (F | i))) \/ (union {(F . (i + 1))}) by ZFMISC_1:78;
i <= k by A38, NAT_1:13;
then i < len D by A34, XXREAL_0:2;
then A47: i in dom D by A43, FINSEQ_3:25;
then D . i in [.a,b.] by A1, INTEGRA1:6;
then A48: a <= D . i by XXREAL_1:1;
A49: D . i < D . (i + 1) by A44, A47, A40, A6, VALUED_0:def 13;
1 < i + 1 by A42, NAT_1:13, NAT_1:14;
then F . (i + 1) = [.(D . ((i + 1) -' 1)),(D . (i + 1)).[ by A5, A39, A40;
then F . (i + 1) = [.(D . i),(D . (i + 1)).[ by NAT_D:34;
hence union (rng (F | (i + 1))) = [.a,(D . (i + 1)).[ by A46, A48, A49, A37, A42, A38, NAT_1:13, NAT_1:14, XXREAL_1:168; :: thesis: verum

end;

end;

end;

A50: for i being Nat holds S₂[i] from NAT_1:sch 2(A35, A36);
1 <= k by A31, FINSEQ_3:25;
hence union (rng (F | k)) = [.a,(D . k).[ by A50; :: thesis: verum

end;

union (rng F) = A

proof

per cases ( len D = 1 or len D <> 1 ) ;

suppose A51: len D = 1 ; :: thesis: union (rng F) = A

then A52: 1 in dom F by A6, FINSEQ_3:25;
len F = 1 by A51, A5, FINSEQ_1:def 3;
then F = <*(F . 1)*> by FINSEQ_1:40;
then rng F = {(F . 1)} by FINSEQ_1:38;
hence union (rng F) = A by A1, A5, A51, A52; :: thesis: verum

end;

suppose A53: len D <> 1 ; :: thesis: union (rng F) = A

consider k being Nat such that
A54: len D = k + 1 by NAT_1:6;
A55: 1 <= len D by FINSEQ_1:20;
then 1 < len D by A53, XXREAL_0:1;
then A56: ( 1 <= k & k < len D ) by A54, NAT_1:13;
then A57: k in dom F by A6, FINSEQ_3:25;
A58: union (rng (F | k)) = [.a,(D . k).[ by A56, A30, A6, FINSEQ_3:25;
reconsider a1 = lower_bound A, a2 = upper_bound A as Real ;
A = [.a1,a2.] by INTEGRA1:4;
then A59: b = upper_bound A by A1, INTEGRA1:5;
k + 1 in dom F by A54, A55, A6, FINSEQ_3:25;
then F . (k + 1) = [.(D . ((k + 1) -' 1)),(D . (k + 1)).] by A54, A53, A5;
then F . (k + 1) = [.(D . k),(D . (k + 1)).] by NAT_D:34;
then A60: F . (k + 1) = [.(D . k),b.] by A54, A59, INTEGRA1:def 2;
D . k in A by A57, A6, INTEGRA1:6;
then A61: ( a <= D . k & D . k <= b ) by A1, XXREAL_1:1;
A62: len F = k + 1 by A54, A5, FINSEQ_1:def 3;
F | k = F | (Seg k) by FINSEQ_1:def 16;
then F = (F | k) ^ <*(F . (k + 1))*> by A62, FINSEQ_3:55;
then rng F = (rng (F | k)) \/ (rng <*(F . (k + 1))*>) by FINSEQ_1:31;
then union (rng F) = (union (rng (F | k))) \/ (union (rng <*(F . (k + 1))*>)) by ZFMISC_1:78;
then union (rng F) = [.a,(D . k).[ \/ (union {(F . (k + 1))}) by A58, FINSEQ_1:38;
hence union (rng F) = A by A1, A60, A61, XXREAL_1:166; :: thesis: verum

end;

end;

end;

hence ( dom D = dom F & 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).] ) ) ) ) ) ) by A5, FINSEQ_1:def 3; :: thesis: verum