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 A9, A5, A8, XXREAL_0:1;
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;
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;
end;
end;
|.((D . n) - (D . m)).| <= delta D1
proof
per cases ( n < m or n > m ) by A9, A5, A8, XXREAL_0:1;
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;
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;
end;
end;
hence contradiction by A1, A10, XXREAL_0:2; :: thesis: verum