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_{1}[ 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_{1}[k,x]

A5: ( dom F = Seg (len D) & ( for k being Nat st k in Seg (len D) holds

S_{1}[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

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).[

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

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

A2: for k being Nat st k in Seg (len D) holds

ex x being Element of Borel_Sets st S

proof

consider F being FinSequence of Borel_Sets such that
let k be Nat; :: thesis: ( k in Seg (len D) implies ex x being Element of Borel_Sets st S_{1}[k,x] )

assume k in Seg (len D) ; :: thesis: ex x being Element of Borel_Sets st S_{1}[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_{1}[k,x]
by A3, A4; :: thesis: verum

end;assume k in Seg (len D) ; :: thesis: ex x being Element of Borel_Sets st S

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

A5: ( dom F = Seg (len D) & ( for k being Nat st k in Seg (len D) holds

S

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

then reconsider F = F as Finite_Sep_Sequence of Borel_Sets by PROB_2:def 2;
let x, y be object ; :: thesis: ( x <> y implies F . x misses F . y )

assume A7: x <> y ; :: thesis: F . x misses F . y

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

end;

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;hence F . x misses F . y by XBOOLE_1:65; :: thesis: verum

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;

end;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;then ( x1 = 1 & y1 = 1 ) by A10, XXREAL_0:1;

hence contradiction by A7; :: thesis: verum

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

end;

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

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;

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

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

end;

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

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

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

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

union (rng F) = A
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_{2}[ Nat] means ( 1 <= $1 & $1 <= k implies union (rng (F | $1)) = [.a,(D . $1).[ );

A35: S_{2}[ 0 ]
;

A36: for i being Nat st S_{2}[i] holds

S_{2}[i + 1]
_{2}[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;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

A35: S

A36: for i being Nat st S

S

proof

A50:
for i being Nat holds S
let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume A37: S_{2}[i]
; :: thesis: S_{2}[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;

end;assume A37: S

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

end;

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

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

1 <= k by A31, FINSEQ_3:25;

hence union (rng (F | k)) = [.a,(D . k).[ by A50; :: thesis: verum

proof
end;

hence
( dom D = dom F & union (rng F) = A & ( for k being Nat st k in dom F holds per cases
( len D = 1 or len D <> 1 )
;

end;

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

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

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

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

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