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 S1[ 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 S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len D) implies ex x being Element of Borel_Sets st S1[k,x] )
assume k in Seg (len D) ; :: thesis: ex x being Element of Borel_Sets st S1[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 S1[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
S1[k,F . k] ) ) from A6: dom F = dom D by ;
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 ;
A10: ( 1 <= x1 & x1 <= len D & 1 <= y1 & y1 <= len D ) by ;
A11: now :: thesis: not len D = 1
assume len D = 1 ; :: thesis: contradiction
then ( x1 = 1 & y1 = 1 ) by ;
hence contradiction by A7; :: thesis: verum
end;
per cases ( 1 = x1 or ( 1 < x1 & x1 < len D ) or x1 = len D ) by ;
suppose A12: 1 = x1 ; :: thesis: F . x misses F . y
then A13: ( 1 < y1 & y1 <= len D ) by ;
then A14: ( x1 <= y1 -' 1 & y1 -' 1 <= len D ) by ;
then A15: y1 -' 1 in dom D by ;
A16: F . x = [.a,(D . x1).[ by A8, A5, A12, A11;
( y1 < len D or y1 = len D ) by ;
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 ; :: 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 ;
per cases ( x1 < y1 or x1 > y1 ) by ;
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 ;
then A21: y1 -' 1 in dom D by FINSEQ_3:25;
( y1 = len D or ( 1 < y1 & y1 < len D ) ) by ;
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 ; :: 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 ;
then A24: x1 -' 1 in dom D by FINSEQ_3:25;
( y1 = 1 or ( 1 < y1 & y1 < len D ) ) by ;
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 ; :: 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 ;
then A28: y1 <= x1 -' 1 by ;
then ( 1 <= x1 -' 1 & x1 -' 1 <= len D ) by ;
then A29: x1 -' 1 in dom D by FINSEQ_3:25;
( y1 = 1 or 1 < y1 ) by ;
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 ; :: 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 ;
len D = len F by ;
then A34: k < len D by ;
defpred S2[ Nat] means ( 1 <= \$1 & \$1 <= k implies union (rng (F | \$1)) = [.a,(D . \$1).[ );
A35: S2[ 0 ] ;
A36: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A37: S2[i] ; :: thesis: S2[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 ;
i + 1 <= len F by ;
then A40: i + 1 in dom F by ;
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 ;
then F | (i + 1) = <*((F | (i + 1)) . 1)*> by FINSEQ_1:40;
then F | (i + 1) = <*(F . 1)*> by ;
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 15;
len (F | (i + 1)) = i + 1 by ;
then F | (i + 1) = (F | i) ^ <*((F | (i + 1)) . (i + 1))*> by ;
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 ;
then i < len D by ;
then A47: i in dom D by ;
then D . i in [.a,b.] by ;
then A48: a <= D . i by XXREAL_1:1;
A49: D . i < D . (i + 1) by ;
1 < i + 1 by ;
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 ; :: thesis: verum
end;
end;
end;
A50: for i being Nat holds S2[i] from 1 <= k by ;
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 ;
len F = 1 by ;
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 ;
then A56: ( 1 <= k & k < len D ) by ;
then A57: k in dom F by ;
A58: union (rng (F | k)) = [.a,(D . k).[ by ;
reconsider a1 = lower_bound A, a2 = upper_bound A as Real ;
A = [.a1,a2.] by INTEGRA1:4;
then A59: b = upper_bound A by ;
k + 1 in dom F by ;
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 ;
D . k in A by ;
then A61: ( a <= D . k & D . k <= b ) by ;
A62: len F = k + 1 by ;
F | k = F | (Seg k) by FINSEQ_1:def 15;
then F = (F | k) ^ <*(F . (k + 1))*> by ;
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 ;
hence union (rng F) = A by ; :: 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 ; :: thesis: verum