let a, b, c be Real; :: thesis: for Iac, Icb being non empty compact Subset of REAL st a <= c & c <= b & Iac = [.a,c.] & Icb = [.c,b.] holds
for Dac being Division of Iac
for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb holds
( ( i < len Dac implies Dac . i < Dcb . j ) & ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) )
let Iac, Icb be non empty compact Subset of REAL; :: thesis: ( a <= c & c <= b & Iac = [.a,c.] & Icb = [.c,b.] implies for Dac being Division of Iac
for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb holds
( ( i < len Dac implies Dac . i < Dcb . j ) & ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) ) )
assume that
A1: ( a <= c & c <= b ) and
A2: Iac = [.a,c.] and
A3: Icb = [.c,b.] ; :: thesis: for Dac being Division of Iac
for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb holds
( ( i < len Dac implies Dac . i < Dcb . j ) & ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) )
let Dac be Division of Iac; :: thesis: for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb holds
( ( i < len Dac implies Dac . i < Dcb . j ) & ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) )
let Dcb be Division of Icb; :: thesis: for i, j being Nat st i in dom Dac & j in dom Dcb holds
( ( i < len Dac implies Dac . i < Dcb . j ) & ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) )
let i, j be Nat; :: thesis: ( i in dom Dac & j in dom Dcb implies ( ( i < len Dac implies Dac . i < Dcb . j ) & ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) ) )
assume that
A4: i in dom Dac and
A5: j in dom Dcb ; :: thesis: ( ( i < len Dac implies Dac . i < Dcb . j ) & ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) )
A6: Dac . (len Dac) = upper_bound Iac by INTEGRA1:def 2
.= c by A1, A2, JORDAN5A:19 ;
rng Dcb c= [.c,b.] by A3, INTEGRA1:def 2;
then Dcb . j in [.c,b.] by A5, FUNCT_1:3;
then A7: c <= Dcb . j by XXREAL_1:1;
thus ( i < len Dac implies Dac . i < Dcb . j ) :: thesis: ( ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) )
proof
assume A8: i < len Dac ; :: thesis: Dac . i < Dcb . j
Seg (len Dac) = dom Dac by FINSEQ_1:def 3;
then len Dac in dom Dac by FINSEQ_1:3;
then Dac . i < c by A6, A8, A4, VALUED_0:def 13;
hence Dac . i < Dcb . j by A7, XXREAL_0:2; :: thesis: verum
end;
thus ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) :: thesis: ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 )
proof
assume A9: ( i = len Dac & c < Dcb . 1 ) ; :: thesis: Dac . i < Dcb . j
A10: 1 in dom Dcb by FINSEQ_5:6;
j in Seg (len Dcb) by A5, FINSEQ_1:def 3;
then not not j = 1 & ... & not j = len Dcb by FINSEQ_1:91;
per cases then ( j = 1 or 1 < j ) by XXREAL_0:1;
suppose j = 1 ; :: thesis: Dac . i < Dcb . j
hence Dac . i < Dcb . j by A9, A6; :: thesis: verum
end;
suppose 1 < j ; :: thesis: Dac . i < Dcb . j
then Dcb . 1 < Dcb . j by A10, A5, VALUED_0:def 13;
hence Dac . i < Dcb . j by A9, A6, XXREAL_0:2; :: thesis: verum
end;
end;
end;
thus ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) by A6; :: thesis: verum