let A be closed-interval Subset of REAL ; :: thesis: for D1, D being Division of A st delta D1 < min (rng (upper_volume (chi A,A),D)) holds
for x, y being Real
for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset D1,i) & y in (rng D) /\ (divset D1,i) holds
x = y
let D1, D be Division of A; :: thesis: ( delta D1 < min (rng (upper_volume (chi A,A),D)) implies for x, y being Real
for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset D1,i) & y in (rng D) /\ (divset D1,i) holds
x = y )
assume A1: delta D1 < min (rng (upper_volume (chi A,A),D)) ; :: thesis: for x, y being Real
for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset D1,i) & y in (rng D) /\ (divset D1,i) holds
x = y
let x, y be Real; :: thesis: for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset D1,i) & y in (rng D) /\ (divset D1,i) holds
x = y
let i be Element of NAT ; :: thesis: ( i in dom D1 & x in (rng D) /\ (divset D1,i) & y in (rng D) /\ (divset D1,i) implies x = y )
assume A2: i in dom D1 ; :: thesis: ( not x in (rng D) /\ (divset D1,i) or not y in (rng D) /\ (divset D1,i) or x = y )
assume A3: x in (rng D) /\ (divset D1,i) ; :: thesis: ( not y in (rng D) /\ (divset D1,i) or x = y )
assume A4: y in (rng D) /\ (divset D1,i) ; :: thesis: x = y
assume A5: x <> y ; :: thesis: contradiction
x in rng D by A3, XBOOLE_0:def 4;
then consider n being Element of NAT such that
A6: ( n in dom D & x = D . n ) by PARTFUN1:26;
y in rng D by A4, XBOOLE_0:def 4;
then consider m being Element of NAT such that
A7: ( m in dom D & y = D . m ) by PARTFUN1:26;
A8: abs ((D . n) - (D . m)) >= min (rng (upper_volume (chi A,A),D))

proof

per cases ( n < m or n > m ) by A5, A6, A7, XXREAL_0:1;

suppose n < m ; :: thesis: abs ((D . n) - (D . m)) >= min (rng (upper_volume (chi A,A),D))

then A9: n + 1 <= m by NAT_1:13;
( n in Seg (len D) & m in Seg (len D) ) by A6, A7, FINSEQ_1:def 3;
then A10: ( 1 <= n & m <= len D ) by FINSEQ_1:3;
then ( 1 <= n + 1 & n + 1 <= len D ) by A9, NAT_1:12, XXREAL_0:2;
then A11: n + 1 in Seg (len D) by FINSEQ_1:3;
then A12: n + 1 in dom D by FINSEQ_1:def 3;
- (abs ((D . n) - (D . m))) <= (D . n) - (D . m) by ABSVALUE:11;
then A13: abs ((D . n) - (D . m)) >= - ((D . n) - (D . m)) by XREAL_1:28;
D . m >= D . (n + 1) by A7, A9, A12, GOBOARD2:18;
then (D . n) - (D . m) <= (D . n) - (D . (n + 1)) by XREAL_1:12;
then A14: - ((D . n) - (D . m)) >= - ((D . n) - (D . (n + 1))) by XREAL_1:26;
A15: (D . (n + 1)) - (D . n) = (upper_volume (chi A,A),D) . (n + 1)

proof

n + 1 <> 1 by A10, NAT_1:13;
then ( lower_bound (divset D,(n + 1)) = D . ((n + 1) - 1) & upper_bound (divset D,(n + 1)) = D . (n + 1) ) by A12, INTEGRA1:def 5;
then vol (divset D,(n + 1)) = (D . (n + 1)) - (D . n) by INTEGRA1:def 6;
hence (D . (n + 1)) - (D . n) = (upper_volume (chi A,A),D) . (n + 1) by A12, INTEGRA1:22; :: thesis: verum

end;

n + 1 in Seg (len (upper_volume (chi A,A),D)) by A11, INTEGRA1:def 7;
then n + 1 in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
then (upper_volume (chi A,A),D) . (n + 1) in rng (upper_volume (chi A,A),D) by FUNCT_1:def 5;
then (D . (n + 1)) - (D . n) >= min (rng (upper_volume (chi A,A),D)) by A15, XXREAL_2:def 7;
then - ((D . n) - (D . m)) >= min (rng (upper_volume (chi A,A),D)) by A14, XXREAL_0:2;
hence abs ((D . n) - (D . m)) >= min (rng (upper_volume (chi A,A),D)) by A13, XXREAL_0:2; :: thesis: verum

end;

suppose n > m ; :: thesis: abs ((D . n) - (D . m)) >= min (rng (upper_volume (chi A,A),D))

then A16: m + 1 <= n by NAT_1:13;
( n in Seg (len D) & m in Seg (len D) ) by A6, A7, FINSEQ_1:def 3;
then A17: ( 1 <= m & n <= len D ) by FINSEQ_1:3;
then A18: ( 1 <= m + 1 & m + 1 <= len D ) by A16, NAT_1:12, XXREAL_0:2;
then A19: m + 1 in Seg (len D) by FINSEQ_1:3;
A20: m + 1 in dom D by A18, FINSEQ_3:27;
A21: abs ((D . n) - (D . m)) >= (D . n) - (D . m) by ABSVALUE:11;
D . (m + 1) <= D . n by A6, A16, A20, GOBOARD2:18;
then A22: (D . n) - (D . m) >= (D . (m + 1)) - (D . m) by XREAL_1:11;
A23: (D . (m + 1)) - (D . m) = (upper_volume (chi A,A),D) . (m + 1)

proof

1 < m + 1 by A17, NAT_1:13;
then ( lower_bound (divset D,(m + 1)) = D . ((m + 1) - 1) & upper_bound (divset D,(m + 1)) = D . (m + 1) ) by A20, INTEGRA1:def 5;
then vol (divset D,(m + 1)) = (D . (m + 1)) - (D . m) by INTEGRA1:def 6;
hence (D . (m + 1)) - (D . m) = (upper_volume (chi A,A),D) . (m + 1) by A20, INTEGRA1:22; :: thesis: verum

end;

m + 1 in Seg (len (upper_volume (chi A,A),D)) by A19, INTEGRA1:def 7;
then m + 1 in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
then (upper_volume (chi A,A),D) . (m + 1) in rng (upper_volume (chi A,A),D) by FUNCT_1:def 5;
then (D . (m + 1)) - (D . m) >= min (rng (upper_volume (chi A,A),D)) by A23, XXREAL_2:def 7;
then (D . n) - (D . m) >= min (rng (upper_volume (chi A,A),D)) by A22, XXREAL_0:2;
hence abs ((D . n) - (D . m)) >= min (rng (upper_volume (chi A,A),D)) by A21, XXREAL_0:2; :: thesis: verum

end;

end;

end;

abs ((D . n) - (D . m)) <= delta D1

proof

per cases ( n < m or n > m ) by A5, A6, A7, XXREAL_0:1;

suppose n < m ; :: thesis: abs ((D . n) - (D . m)) <= delta D1

then D . n < D . m by A6, A7, SEQM_3:def 1;
then (D . n) - (D . m) < 0 by XREAL_1:51;
then A24: abs ((D . n) - (D . m)) = - ((D . n) - (D . m)) by ABSVALUE:def 1
.= (D . m) - (D . n) ;
D . n in divset D1,i by A3, A6, XBOOLE_0:def 4;
then A25: D . n >= lower_bound (divset D1,i) by INTEGRA2:1;
D . m in divset D1,i by A4, A7, XBOOLE_0:def 4;
then D . m <= upper_bound (divset D1,i) by INTEGRA2:1;
then A26: (D . m) - (lower_bound (divset D1,i)) <= (upper_bound (divset D1,i)) - (lower_bound (divset D1,i)) by XREAL_1:11;
(D . m) - (D . n) <= (D . m) - (lower_bound (divset D1,i)) by A25, XREAL_1:12;
then (D . m) - (D . n) <= (upper_bound (divset D1,i)) - (lower_bound (divset D1,i)) by A26, XXREAL_0:2;
then A27: (D . m) - (D . n) <= vol (divset D1,i) by INTEGRA1:def 6;
A28: i in Seg (len D1) by A2, FINSEQ_1:def 3;
A29: (D . m) - (D . n) <= (upper_volume (chi A,A),D1) . i by A27, A2, INTEGRA1:22;
i in Seg (len (upper_volume (chi A,A),D1)) by A28, INTEGRA1:def 7;
then i in dom (upper_volume (chi A,A),D1) by FINSEQ_1:def 3;
then (upper_volume (chi A,A),D1) . i in rng (upper_volume (chi A,A),D1) by FUNCT_1:def 5;
then (upper_volume (chi A,A),D1) . i <= max (rng (upper_volume (chi A,A),D1)) by XXREAL_2:def 8;
then (upper_volume (chi A,A),D1) . i <= delta D1 by INTEGRA1:def 19;
hence abs ((D . n) - (D . m)) <= delta D1 by A24, A29, XXREAL_0:2; :: thesis: verum

end;

suppose n > m ; :: thesis: abs ((D . n) - (D . m)) <= delta D1

then D . n > D . m by A6, A7, SEQM_3:def 1;
then (D . n) - (D . m) > 0 by XREAL_1:52;
then A30: abs ((D . n) - (D . m)) = (D . n) - (D . m) by ABSVALUE:def 1;
D . m in divset D1,i by A4, A7, XBOOLE_0:def 4;
then A31: D . m >= lower_bound (divset D1,i) by INTEGRA2:1;
D . n in divset D1,i by A3, A6, XBOOLE_0:def 4;
then D . n <= upper_bound (divset D1,i) by INTEGRA2:1;
then A32: (D . n) - (lower_bound (divset D1,i)) <= (upper_bound (divset D1,i)) - (lower_bound (divset D1,i)) by XREAL_1:11;
(D . n) - (D . m) <= (D . n) - (lower_bound (divset D1,i)) by A31, XREAL_1:12;
then (D . n) - (D . m) <= (upper_bound (divset D1,i)) - (lower_bound (divset D1,i)) by A32, XXREAL_0:2;
then A33: (D . n) - (D . m) <= vol (divset D1,i) by INTEGRA1:def 6;
A34: i in Seg (len D1) by A2, FINSEQ_1:def 3;
A35: (D . n) - (D . m) <= (upper_volume (chi A,A),D1) . i by A33, A2, INTEGRA1:22;
i in Seg (len (upper_volume (chi A,A),D1)) by A34, INTEGRA1:def 7;
then i in dom (upper_volume (chi A,A),D1) by FINSEQ_1:def 3;
then (upper_volume (chi A,A),D1) . i in rng (upper_volume (chi A,A),D1) by FUNCT_1:def 5;
then (upper_volume (chi A,A),D1) . i <= max (rng (upper_volume (chi A,A),D1)) by XXREAL_2:def 8;
then (upper_volume (chi A,A),D1) . i <= delta D1 by INTEGRA1:def 19;
hence abs ((D . n) - (D . m)) <= delta D1 by A30, A35, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction by A1, A8, XXREAL_0:2; :: thesis: verum