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

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

|.((D . n) - (D . m)).| <= delta D1
per cases
( n < m or n > m )
by A9, A5, A8, XXREAL_0:1;

end;

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 A7, FINSEQ_1:def 3;

then m <= len D by FINSEQ_1:1;

then n + 1 <= len D by A11, XXREAL_0:2;

then A13: n + 1 in Seg (len D) by A12, FINSEQ_1:1;

then A14: n + 1 in dom D by FINSEQ_1:def 3;

then D . m >= D . (n + 1) by A7, A11, SEQ_4:137;

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 A13, INTEGRA1:def 6;

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 A4, FINSEQ_1:def 3;

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 A14, INTEGRA1:def 4;

- |.((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 A14, A17, INTEGRA1:def 4;

then vol (divset (D,(n + 1))) = (D . (n + 1)) - (D . n) by A18, INTEGRA1:def 5;

then (D . (n + 1)) - (D . n) = (upper_volume ((chi (A,A)),D)) . (n + 1) by A14, INTEGRA1:20;

then (D . (n + 1)) - (D . n) >= min (rng (upper_volume ((chi (A,A)),D))) by A16, XXREAL_2:def 7;

then - ((D . n) - (D . m)) >= min (rng (upper_volume ((chi (A,A)),D))) by A15, XXREAL_0:2;

hence |.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D))) by A19, XXREAL_0:2; :: thesis: verum

end;A12: 1 <= n + 1 by NAT_1:12;

m in Seg (len D) by A7, FINSEQ_1:def 3;

then m <= len D by FINSEQ_1:1;

then n + 1 <= len D by A11, XXREAL_0:2;

then A13: n + 1 in Seg (len D) by A12, FINSEQ_1:1;

then A14: n + 1 in dom D by FINSEQ_1:def 3;

then D . m >= D . (n + 1) by A7, A11, SEQ_4:137;

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 A13, INTEGRA1:def 6;

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 A4, FINSEQ_1:def 3;

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 A14, INTEGRA1:def 4;

- |.((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 A14, A17, INTEGRA1:def 4;

then vol (divset (D,(n + 1))) = (D . (n + 1)) - (D . n) by A18, INTEGRA1:def 5;

then (D . (n + 1)) - (D . n) = (upper_volume ((chi (A,A)),D)) . (n + 1) by A14, INTEGRA1:20;

then (D . (n + 1)) - (D . n) >= min (rng (upper_volume ((chi (A,A)),D))) by A16, XXREAL_2:def 7;

then - ((D . n) - (D . m)) >= min (rng (upper_volume ((chi (A,A)),D))) by A15, XXREAL_0:2;

hence |.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D))) by A19, XXREAL_0:2; :: thesis: verum

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 A4, FINSEQ_1:def 3;

then n <= len D by FINSEQ_1:1;

then A21: m + 1 <= len D by A20, XXREAL_0:2;

A22: 1 <= m + 1 by NAT_1:12;

then A23: m + 1 in dom D by A21, FINSEQ_3:25;

then D . (m + 1) <= D . n by A4, A20, SEQ_4:137;

then A24: (D . n) - (D . m) >= (D . (m + 1)) - (D . m) by XREAL_1:9;

m + 1 in Seg (len D) by A22, A21, FINSEQ_1:1;

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 A7, FINSEQ_1:def 3;

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 A23, INTEGRA1:def 4;

lower_bound (divset (D,(m + 1))) = D . ((m + 1) - 1) by A23, A26, INTEGRA1:def 4;

then vol (divset (D,(m + 1))) = (D . (m + 1)) - (D . m) by A27, INTEGRA1:def 5;

then (D . (m + 1)) - (D . m) = (upper_volume ((chi (A,A)),D)) . (m + 1) by A23, INTEGRA1:20;

then (D . (m + 1)) - (D . m) >= min (rng (upper_volume ((chi (A,A)),D))) by A25, XXREAL_2:def 7;

then A28: (D . n) - (D . m) >= min (rng (upper_volume ((chi (A,A)),D))) by A24, XXREAL_0:2;

|.((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 A28, XXREAL_0:2; :: thesis: verum

end;n in Seg (len D) by A4, FINSEQ_1:def 3;

then n <= len D by FINSEQ_1:1;

then A21: m + 1 <= len D by A20, XXREAL_0:2;

A22: 1 <= m + 1 by NAT_1:12;

then A23: m + 1 in dom D by A21, FINSEQ_3:25;

then D . (m + 1) <= D . n by A4, A20, SEQ_4:137;

then A24: (D . n) - (D . m) >= (D . (m + 1)) - (D . m) by XREAL_1:9;

m + 1 in Seg (len D) by A22, A21, FINSEQ_1:1;

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 A7, FINSEQ_1:def 3;

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 A23, INTEGRA1:def 4;

lower_bound (divset (D,(m + 1))) = D . ((m + 1) - 1) by A23, A26, INTEGRA1:def 4;

then vol (divset (D,(m + 1))) = (D . (m + 1)) - (D . m) by A27, INTEGRA1:def 5;

then (D . (m + 1)) - (D . m) = (upper_volume ((chi (A,A)),D)) . (m + 1) by A23, INTEGRA1:20;

then (D . (m + 1)) - (D . m) >= min (rng (upper_volume ((chi (A,A)),D))) by A25, XXREAL_2:def 7;

then A28: (D . n) - (D . m) >= min (rng (upper_volume ((chi (A,A)),D))) by A24, XXREAL_0:2;

|.((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 A28, XXREAL_0:2; :: thesis: verum

proof
end;

hence
contradiction
by A1, A10, XXREAL_0:2; :: thesis: verumper cases
( n < m or n > m )
by A9, A5, A8, XXREAL_0:1;

end;

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

i in Seg (len D1)
by A2, FINSEQ_1:def 3;

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 A6, A8, XBOOLE_0:def 4;

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 A3, A5, XBOOLE_0:def 4;

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 A31, XXREAL_0:2;

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 A2, INTEGRA1:20;

D . n < D . m by A4, A7, A29, SEQM_3:def 1;

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 A32, A30, XXREAL_0:2; :: thesis: verum

end;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 A6, A8, XBOOLE_0:def 4;

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 A3, A5, XBOOLE_0:def 4;

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 A31, XXREAL_0:2;

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 A2, INTEGRA1:20;

D . n < D . m by A4, A7, A29, SEQM_3:def 1;

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 A32, A30, XXREAL_0:2; :: thesis: verum

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

i in Seg (len D1)
by A2, FINSEQ_1:def 3;

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 A3, A5, XBOOLE_0:def 4;

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 A6, A8, XBOOLE_0:def 4;

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 A35, XXREAL_0:2;

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 A2, INTEGRA1:20;

D . n > D . m by A4, A7, A33, SEQM_3:def 1;

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 A36, A34, XXREAL_0:2; :: thesis: verum

end;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 A3, A5, XBOOLE_0:def 4;

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 A6, A8, XBOOLE_0:def 4;

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 A35, XXREAL_0:2;

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 A2, INTEGRA1:20;

D . n > D . m by A4, A7, A33, SEQM_3:def 1;

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 A36, A34, XXREAL_0:2; :: thesis: verum