let A be non empty closed_interval Subset of REAL; :: thesis: for D, D1 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 D, D1 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 )
then x in rng D by XBOOLE_0:def 4;
then consider n being Element of NAT such that
A4: n in dom D and
A5: x = D . n by PARTFUN1:3;
assume A6: y in (rng D) /\ (divset (D1,i)) ; :: thesis: x = y
then y in rng D by XBOOLE_0:def 4;
then consider m being Element of NAT such that
A7: m in dom D and
A8: y = D . m by PARTFUN1:3;
assume A9: x <> y ; :: thesis: contradiction
A10: |.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D)))
proof
per cases ( n < m or n > m ) by ;
suppose n < m ; :: thesis: |.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D)))
then A11: n + 1 <= m by NAT_1:13;
A12: 1 <= n + 1 by NAT_1:12;
m in Seg (len D) by ;
then m <= len D by FINSEQ_1:1;
then n + 1 <= len D by ;
then A13: n + 1 in Seg (len D) by ;
then A14: n + 1 in dom D by FINSEQ_1:def 3;
then D . m >= D . (n + 1) by ;
then (D . n) - (D . m) <= (D . n) - (D . (n + 1)) by XREAL_1:10;
then A15: - ((D . n) - (D . m)) >= - ((D . n) - (D . (n + 1))) by XREAL_1:24;
n + 1 in Seg (len (upper_volume ((chi (A,A)),D))) by ;
then n + 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
then A16: (upper_volume ((chi (A,A)),D)) . (n + 1) in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;
n in Seg (len D) by ;
then 1 <= n by FINSEQ_1:1;
then A17: n + 1 <> 1 by NAT_1:13;
then A18: upper_bound (divset (D,(n + 1))) = D . (n + 1) by ;
- |.((D . n) - (D . m)).| <= (D . n) - (D . m) by ABSVALUE:4;
then A19: |.((D . n) - (D . m)).| >= - ((D . n) - (D . m)) by XREAL_1:26;
lower_bound (divset (D,(n + 1))) = D . ((n + 1) - 1) by ;
then vol (divset (D,(n + 1))) = (D . (n + 1)) - (D . n) by ;
then (D . (n + 1)) - (D . n) = (upper_volume ((chi (A,A)),D)) . (n + 1) by ;
then (D . (n + 1)) - (D . n) >= min (rng (upper_volume ((chi (A,A)),D))) by ;
then - ((D . n) - (D . m)) >= min (rng (upper_volume ((chi (A,A)),D))) by ;
hence |.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D))) by ; :: thesis: verum
end;
suppose n > m ; :: thesis: |.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D)))
then A20: m + 1 <= n by NAT_1:13;
n in Seg (len D) by ;
then n <= len D by FINSEQ_1:1;
then A21: m + 1 <= len D by ;
A22: 1 <= m + 1 by NAT_1:12;
then A23: m + 1 in dom D by ;
then D . (m + 1) <= D . n by ;
then A24: (D . n) - (D . m) >= (D . (m + 1)) - (D . m) by XREAL_1:9;
m + 1 in Seg (len D) by ;
then m + 1 in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;
then m + 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
then A25: (upper_volume ((chi (A,A)),D)) . (m + 1) in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;
m in Seg (len D) by ;
then 1 <= m by FINSEQ_1:1;
then A26: 1 < m + 1 by NAT_1:13;
then A27: upper_bound (divset (D,(m + 1))) = D . (m + 1) by ;
lower_bound (divset (D,(m + 1))) = D . ((m + 1) - 1) by ;
then vol (divset (D,(m + 1))) = (D . (m + 1)) - (D . m) by ;
then (D . (m + 1)) - (D . m) = (upper_volume ((chi (A,A)),D)) . (m + 1) by ;
then (D . (m + 1)) - (D . m) >= min (rng (upper_volume ((chi (A,A)),D))) by ;
then A28: (D . n) - (D . m) >= min (rng (upper_volume ((chi (A,A)),D))) by ;
|.((D . n) - (D . m)).| >= (D . n) - (D . m) by ABSVALUE:4;
hence |.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D))) by ; :: thesis: verum
end;
end;
end;
|.((D . n) - (D . m)).| <= delta D1
proof
per cases ( n < m or n > m ) by ;
suppose A29: n < m ; :: thesis: |.((D . n) - (D . m)).| <= delta D1
i in Seg (len D1) by ;
then i in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;
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 3;
then (upper_volume ((chi (A,A)),D1)) . i <= max (rng (upper_volume ((chi (A,A)),D1))) by XXREAL_2:def 8;
then A30: (upper_volume ((chi (A,A)),D1)) . i <= delta D1 ;
D . m in divset (D1,i) by ;
then D . m <= upper_bound (divset (D1,i)) by INTEGRA2:1;
then A31: (D . m) - (lower_bound (divset (D1,i))) <= (upper_bound (divset (D1,i))) - (lower_bound (divset (D1,i))) by XREAL_1:9;
D . n in divset (D1,i) by ;
then D . n >= lower_bound (divset (D1,i)) by INTEGRA2:1;
then (D . m) - (D . n) <= (D . m) - (lower_bound (divset (D1,i))) by XREAL_1:10;
then (D . m) - (D . n) <= (upper_bound (divset (D1,i))) - (lower_bound (divset (D1,i))) by ;
then (D . m) - (D . n) <= vol (divset (D1,i)) by INTEGRA1:def 5;
then A32: (D . m) - (D . n) <= (upper_volume ((chi (A,A)),D1)) . i by ;
D . n < D . m by ;
then (D . n) - (D . m) < 0 by XREAL_1:49;
then |.((D . n) - (D . m)).| = - ((D . n) - (D . m)) by ABSVALUE:def 1
.= (D . m) - (D . n) ;
hence |.((D . n) - (D . m)).| <= delta D1 by ; :: thesis: verum
end;
suppose A33: n > m ; :: thesis: |.((D . n) - (D . m)).| <= delta D1
i in Seg (len D1) by ;
then i in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;
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 3;
then (upper_volume ((chi (A,A)),D1)) . i <= max (rng (upper_volume ((chi (A,A)),D1))) by XXREAL_2:def 8;
then A34: (upper_volume ((chi (A,A)),D1)) . i <= delta D1 ;
D . n in divset (D1,i) by ;
then D . n <= upper_bound (divset (D1,i)) by INTEGRA2:1;
then A35: (D . n) - (lower_bound (divset (D1,i))) <= (upper_bound (divset (D1,i))) - (lower_bound (divset (D1,i))) by XREAL_1:9;
D . m in divset (D1,i) by ;
then D . m >= lower_bound (divset (D1,i)) by INTEGRA2:1;
then (D . n) - (D . m) <= (D . n) - (lower_bound (divset (D1,i))) by XREAL_1:10;
then (D . n) - (D . m) <= (upper_bound (divset (D1,i))) - (lower_bound (divset (D1,i))) by ;
then (D . n) - (D . m) <= vol (divset (D1,i)) by INTEGRA1:def 5;
then A36: (D . n) - (D . m) <= (upper_volume ((chi (A,A)),D1)) . i by ;
D . n > D . m by ;
then (D . n) - (D . m) > 0 by XREAL_1:50;
then |.((D . n) - (D . m)).| = (D . n) - (D . m) by ABSVALUE:def 1;
hence |.((D . n) - (D . m)).| <= delta D1 by ; :: thesis: verum
end;
end;
end;
hence contradiction by A1, A10, XXREAL_0:2; :: thesis: verum