let n be Nat; :: thesis: for a, b being Real
for F being FinSequence of REAL st n > 1 & len F = n + 1 & ( for k being Nat st k in dom F holds
( a < F . k & F . k <= b ) ) holds
ex i, j being Nat st
( i in dom F & j in dom F & i <> j & F . i <= F . j & (F . j) - (F . i) < (b - a) / n )
let a, b be Real; :: thesis: for F being FinSequence of REAL st n > 1 & len F = n + 1 & ( for k being Nat st k in dom F holds
( a < F . k & F . k <= b ) ) holds
ex i, j being Nat st
( i in dom F & j in dom F & i <> j & F . i <= F . j & (F . j) - (F . i) < (b - a) / n )
let F be FinSequence of REAL ; :: thesis: ( n > 1 & len F = n + 1 & ( for k being Nat st k in dom F holds
( a < F . k & F . k <= b ) ) implies ex i, j being Nat st
( i in dom F & j in dom F & i <> j & F . i <= F . j & (F . j) - (F . i) < (b - a) / n ) )
assume that
A1: ( n > 1 & len F = n + 1 ) and
A2: for k being Nat st k in dom F holds
( a < F . k & F . k <= b ) ; :: thesis: ex i, j being Nat st
( i in dom F & j in dom F & i <> j & F . i <= F . j & (F . j) - (F . i) < (b - a) / n )
1 <= n + 1 by NAT_1:11;
then 1 in dom F by A1, FINSEQ_3:25;
then ( a < F . 1 & F . 1 <= b ) by A2;
then a < b by XXREAL_0:2;
then A3: a - a < b - a by XREAL_1:9;
deffunc H1( Nat) -> set = ].(a + ((($1 - 1) * (b - a)) / n)),(a + (($1 * (b - a)) / n)).];
defpred S1[ object , object ] means for k being Nat st $1 in H1(k) holds
k = $2;
A4: for x being object st x in ].a,b.] holds
ex k being Nat st
( x in H1(k) & k in Seg n )
proof
let x be object ; :: thesis: ( x in ].a,b.] implies ex k being Nat st
( x in H1(k) & k in Seg n ) )
assume A5: x in ].a,b.] ; :: thesis: ex k being Nat st
( x in H1(k) & k in Seg n )
reconsider x = x as Real by A5;
set k = [/(((x - a) / (b - a)) * n)\];
x > a by A5, XXREAL_1:2;
then A6: x - a > 0 by XREAL_1:50;
A7: [/(((x - a) / (b - a)) * n)\] > 0 by INT_1:def 7, A6, A1, A3;
then A8: [/(((x - a) / (b - a)) * n)\] >= 1 by NAT_1:14;
reconsider k = [/(((x - a) / (b - a)) * n)\] as Element of NAT by A7, INT_1:3;
x <= b by A5, XXREAL_1:2;
then x - a <= b - a by XREAL_1:9;
then (x - a) / (b - a) <= 1 by A6, XREAL_1:183;
then A9: ((x - a) / (b - a)) * n <= 1 * n by XREAL_1:64;
A10: (((x - a) / (b - a)) * n) + 1 <= n + 1 by XREAL_1:7, A9;
k < (((x - a) / (b - a)) * n) + 1 by INT_1:def 7;
then k < n + 1 by A10, XXREAL_0:2;
then A11: k <= n by NAT_1:13;
A12: n / n = 1 by A1, XCMPLX_1:60;
k < (((x - a) / (b - a)) * n) + 1 by INT_1:def 7;
then k - 1 < ((((x - a) / (b - a)) * n) + 1) - 1 by XREAL_1:9;
then (k - 1) / n < (((x - a) / (b - a)) * n) / n by A1, XREAL_1:74;
then (k - 1) / n < ((x - a) / (b - a)) * 1 by A12, XCMPLX_1:74;
then ((k - 1) / n) * (b - a) < ((x - a) / (b - a)) * (b - a) by A3, XREAL_1:68;
then ((k - 1) / n) * (b - a) < ((b - a) / (b - a)) * (x - a) by XCMPLX_1:75;
then ((k - 1) / n) * (b - a) < 1 * (x - a) by A3, XCMPLX_1:60;
then ( (((k - 1) / n) * (b - a)) + a < (x - a) + a & (- a) + a = 0 ) by XREAL_1:6;
then A13: a + (((k - 1) * (b - a)) / n) < x by XCMPLX_1:74;
((x - a) / (b - a)) * n <= k by INT_1:def 7;
then (((x - a) / (b - a)) * n) / n <= k / n by XREAL_1:72;
then ((x - a) / (b - a)) * 1 <= k / n by A12, XCMPLX_1:74;
then ((x - a) / (b - a)) * (b - a) <= (k / n) * (b - a) by A3, XREAL_1:64;
then ((b - a) / (b - a)) * (x - a) <= (k / n) * (b - a) by XCMPLX_1:75;
then 1 * (x - a) <= (k / n) * (b - a) by A3, XCMPLX_1:60;
then ( (x - a) + a <= ((k / n) * (b - a)) + a & (- a) + a = 0 ) by XREAL_1:6;
then x <= a + ((k * (b - a)) / n) by XCMPLX_1:74;
then x in H1(k) by A13, XXREAL_1:2;
hence ex k being Nat st
( x in H1(k) & k in Seg n ) by A11, A8, FINSEQ_1:1; :: thesis: verum
end;
A14: for x being object st x in ].a,b.] holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in ].a,b.] implies ex y being object st S1[x,y] )
assume A15: x in ].a,b.] ; :: thesis: ex y being object st S1[x,y]
consider k being Nat such that
A16: ( x in H1(k) & k in Seg n ) by A15, A4;
take y = k; :: thesis: S1[x,y]
let k1 be Nat; :: thesis: ( x in H1(k1) implies k1 = y )
assume A17: x in H1(k1) ; :: thesis: k1 = y
reconsider x = x as Real by A15;
A18: n / n = 1 by A1, XCMPLX_1:60;
1 <= n + 1 by NAT_1:11;
then 1 in dom F by A1, FINSEQ_3:25;
then ( a < F . 1 & F . 1 <= b ) by A2;
then a < b by XXREAL_0:2;
then A19: a - a < b - a by XREAL_1:9;
A20: (b - a) / (b - a) = 1 by A19, XCMPLX_1:60;
( a + (((k1 - 1) * (b - a)) / n) < x & x <= a + ((k * (b - a)) / n) ) by XXREAL_1:2, A16, A17;
then (((k1 - 1) * (b - a)) / n) + a < ((k * (b - a)) / n) + a by XXREAL_0:2;
then A21: ((((k1 - 1) * (b - a)) / n) + a) - a < (((k * (b - a)) / n) + a) - a by XREAL_1:9;
A22: (((k1 - 1) * (b - a)) / n) * n = ((k1 - 1) * ((b - a) / n)) * n by XCMPLX_1:74
.= (k1 - 1) * (((b - a) / n) * n)
.= (k1 - 1) * ((n / n) * (b - a)) by XCMPLX_1:75
.= (k1 - 1) * (b - a) by A18 ;
A23: ((k * (b - a)) / n) * n = (k * ((b - a) / n)) * n by XCMPLX_1:74
.= k * (((b - a) / n) * n)
.= k * ((n / n) * (b - a)) by XCMPLX_1:75
.= k * (b - a) by A18 ;
A24: ((k1 - 1) * (b - a)) / (b - a) = (k1 - 1) * 1 by A20, XCMPLX_1:74;
A25: (k * (b - a)) / (b - a) = k * 1 by A20, XCMPLX_1:74;
(k1 - 1) * (b - a) < k * (b - a) by A21, A1, XREAL_1:68, A22, A23;
then (k1 - 1) * 1 < k * 1 by A24, A25, A19, XREAL_1:74;
then (k1 - 1) + 1 < k + 1 by XREAL_1:6;
then A26: k1 <= k by NAT_1:13;
( a + (((k - 1) * (b - a)) / n) < x & x <= a + ((k1 * (b - a)) / n) ) by XXREAL_1:2, A16, A17;
then a + (((k - 1) * (b - a)) / n) < a + ((k1 * (b - a)) / n) by XXREAL_0:2;
then ((((k - 1) * (b - a)) / n) + a) - a < (((k1 * (b - a)) / n) + a) - a by XREAL_1:9;
then A27: (((k - 1) * (b - a)) / n) * n < ((k1 * (b - a)) / n) * n by A1, XREAL_1:68;
A28: (((k - 1) * (b - a)) / n) * n = ((k - 1) * ((b - a) / n)) * n by XCMPLX_1:74
.= (k - 1) * (((b - a) / n) * n)
.= (k - 1) * ((n / n) * (b - a)) by XCMPLX_1:75
.= (k - 1) * (b - a) by A18 ;
A29: ((k1 * (b - a)) / n) * n = (k1 * ((b - a) / n)) * n by XCMPLX_1:74
.= k1 * (((b - a) / n) * n)
.= k1 * ((n / n) * (b - a)) by XCMPLX_1:75
.= k1 * (b - a) by A18 ;
A30: ((k - 1) * (b - a)) / (b - a) = (k - 1) * 1 by A20, XCMPLX_1:74;
A31: (k1 * (b - a)) / (b - a) = k1 * ((b - a) / (b - a)) by XCMPLX_1:74
.= k1 * 1 by A19, XCMPLX_1:60 ;
(k - 1) * 1 < k1 * 1 by A30, A31, A27, A28, A29, A19, XREAL_1:74;
then (k - 1) + 1 < k1 + 1 by XREAL_1:6;
then k <= k1 by NAT_1:13;
hence k1 = y by XXREAL_0:1, A26; :: thesis: verum
end;
consider f being Function such that
A32: dom f = ].a,b.] and
A33: for x being object st x in ].a,b.] holds
S1[x,f . x] from CLASSES1:sch 1(A14);
 set fF = f * F;
rng F c= dom f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in dom f )
assume x in rng F ; :: thesis: x in dom f
then consider y being object such that
A34: ( y in dom F & F . y = x ) by FUNCT_1:def 3;
reconsider y = y as Nat by A34;
( a < F . y & F . y <= b ) by A2, A34;
hence x in dom f by A34, A32, XXREAL_1:2; :: thesis: verum
end;
then A35: dom (f * F) = dom F by RELAT_1:27;
A36: rng (f * F) c= Seg n
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f * F) or x in Seg n )
assume x in rng (f * F) ; :: thesis: x in Seg n
then consider y being object such that
A37: ( y in dom (f * F) & (f * F) . y = x ) by FUNCT_1:def 3;
reconsider y = y as Nat by A37;
A38: ( (f * F) . y = f . (F . y) & y in dom F & F . y in dom f ) by FUNCT_1:11, FUNCT_1:12, A37;
consider k being Nat such that
A39: ( F . y in H1(k) & k in Seg n ) by A38, A32, A4;
thus x in Seg n by A38, A32, A33, A37, A39; :: thesis: verum
end;
assume A40: for n1, n2 being Nat st n1 in dom F & n2 in dom F & n1 <> n2 & F . n1 <= F . n2 holds
(F . n2) - (F . n1) >= (b - a) / n ; :: thesis: contradiction
A41: f * F is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 (f * F) or not x2 in proj1 (f * F) or not (f * F) . x1 = (f * F) . x2 or x1 = x2 )
assume A42: ( x1 in dom (f * F) & x2 in dom (f * F) & (f * F) . x1 = (f * F) . x2 ) ; :: thesis: x1 = x2
assume A43: x1 <> x2 ; :: thesis: contradiction
A44: ( x1 in dom F & F . x1 in dom f ) by A42, FUNCT_1:11;
A45: ( x2 in dom F & F . x2 in dom f ) by A42, FUNCT_1:11;
reconsider x1 = x1, x2 = x2 as Nat by A42;
A46: (f * F) . x1 = f . (F . x1) by A42, FUNCT_1:12;
consider k1 being Nat such that
A47: ( F . x1 in H1(k1) & k1 in Seg n ) by A4, A44, A32;
consider k2 being Nat such that
A48: ( F . x2 in H1(k2) & k2 in Seg n ) by A4, A45, A32;
( k1 = f . (F . x1) & k2 = f . (F . x2) ) by A47, A48, A44, A45, A33, A32;
then A49: k1 = k2 by A42, A46, FUNCT_1:12;
( F . x1 <= F . x2 or F . x2 <= F . x1 ) ;
then A50: ( (F . x1) - (F . x2) >= (b - a) / n or (F . x2) - (F . x1) >= (b - a) / n ) by A40, A44, A45, A43;
A51: ( F . x1 <= a + ((k1 * (b - a)) / n) & F . x2 > a + (((k1 - 1) * (b - a)) / n) ) by A47, A48, A49, XXREAL_1:2;
A52: (a + ((k1 * (b - a)) / n)) - (a + (((k1 - 1) * (b - a)) / n)) = ((a + ((k1 * (b - a)) / n)) - a) - (((k1 - 1) * (b - a)) / n)
.= (k1 * ((b - a) / n)) - (((k1 - 1) * (b - a)) / n) by XCMPLX_1:74
.= (k1 * ((b - a) / n)) - ((k1 - 1) * ((b - a) / n)) by XCMPLX_1:74
.= (b - a) / n ;
( F . x2 <= a + ((k1 * (b - a)) / n) & F . x1 > a + (((k1 - 1) * (b - a)) / n) ) by A47, A48, A49, XXREAL_1:2;
hence contradiction by A50, A52, A51, XREAL_1:15; :: thesis: verum
end;
A53: card (dom (f * F)) c= card (rng (f * F)) by CARD_1:10, A41;
card (rng (f * F)) c= card (Seg n) by A36, CARD_1:11;
then A54: Segm (card (dom (f * F))) c= Segm (card (Seg n)) by A53;
A55: dom F = Seg (n + 1) by A1, FINSEQ_1:def 3;
A56: ( card (Seg n) = n & card (Seg (n + 1)) = n + 1 ) by FINSEQ_1:57;
n + 1 <= n by A56, A54, A55, A35, NAT_1:39;
hence contradiction by NAT_1:13; :: thesis: verum