let A be closed-interval Subset of REAL ; :: thesis: for D1, D2 being Division of A st D1 <= D2 holds
for j being Element of NAT st j in dom D2 holds
ex i being Element of NAT st
( i in dom D1 & divset D2,j c= divset D1,i )
let D1, D2 be Division of A; :: thesis: ( D1 <= D2 implies for j being Element of NAT st j in dom D2 holds
ex i being Element of NAT st
( i in dom D1 & divset D2,j c= divset D1,i ) )
assume A1: D1 <= D2 ; :: thesis: for j being Element of NAT st j in dom D2 holds
ex i being Element of NAT st
( i in dom D1 & divset D2,j c= divset D1,i )
let j be Element of NAT ; :: thesis: ( j in dom D2 implies ex i being Element of NAT st
( i in dom D1 & divset D2,j c= divset D1,i ) )
assume A2: j in dom D2 ; :: thesis: ex i being Element of NAT st
( i in dom D1 & divset D2,j c= divset D1,i )
defpred S1[ set ] means ( D2 . $1 in rng D1 & D2 . $1 >= D2 . j );
consider X being Subset of (dom D2) such that
A3: for x1 being set holds
( x1 in X iff ( x1 in dom D2 & S1[x1] ) ) from SUBSET_1:sch 1();
 reconsider X = X as Subset of NAT by XBOOLE_1:1;
not X is empty
proof
ex n being Element of NAT st
( n in dom D2 & D2 . n in rng D1 & D2 . n >= D2 . j )
proof
A4: ( len D2 in dom D2 & D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j )
proof
len D2 in Seg (len D2) by FINSEQ_1:5;
hence A5: len D2 in dom D2 by FINSEQ_1:def 3; :: thesis: ( D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j )
len D1 in Seg (len D1) by FINSEQ_1:5;
then A6: len D1 in dom D1 by FINSEQ_1:def 3;
D2 . (len D2) = upper_bound A by INTEGRA1:def 2;
then D1 . (len D1) = D2 . (len D2) by INTEGRA1:def 2;
hence D2 . (len D2) in rng D1 by A6, FUNCT_1:def 5; :: thesis: D2 . (len D2) >= D2 . j
j in Seg (len D2) by A2, FINSEQ_1:def 3;
then j <= len D2 by FINSEQ_1:3;
hence D2 . (len D2) >= D2 . j by A2, A5, GOBOARD2:18; :: thesis: verum
end;
take len D2 ; :: thesis: ( len D2 in dom D2 & D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j )
thus ( len D2 in dom D2 & D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j ) by A4; :: thesis: verum
end;
hence not X is empty by A3; :: thesis: verum
end;
then reconsider X = X as non empty Subset of NAT ;
A7: min X in X by XXREAL_2:def 7;
then A8: ( min X in dom D2 & D2 . (min X) in rng D1 & D2 . (min X) >= D2 . j ) by A3;
then consider i being Element of NAT such that
A9: ( i in dom D1 & D2 . (min X) = D1 . i ) by PARTFUN1:26;
A10: D1 . i >= D2 . j by A3, A7, A9;
A11: divset D2,j c= divset D1,i
proof
now
per cases ( i = 1 or i <> 1 ) ;
suppose i = 1 ; :: thesis: divset D2,j c= divset D1,i
then ( lower_bound (divset D1,i) = lower_bound A & upper_bound (divset D1,i) = D1 . i ) by A9, INTEGRA1:def 5;
then A12: divset D1,i = [.(lower_bound A),(D1 . i).] by INTEGRA1:5;
now
per cases ( j = 1 or j <> 1 ) ;
suppose j = 1 ; :: thesis: divset D2,j c= divset D1,i
then ( lower_bound (divset D2,j) = lower_bound A & upper_bound (divset D2,j) = D2 . j ) by A2, INTEGRA1:def 5;
then A13: divset D2,j = [.(lower_bound A),(D2 . j).] by INTEGRA1:5;
A14: lower_bound A in [.(lower_bound A),(D1 . i).]
proof
A15: D1 . i in rng D1 by A9, FUNCT_1:def 5;
rng D1 c= A by INTEGRA1:def 2;
then A16: D1 . i in A by A15;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:5;
then D1 . i in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A16, RCOMP_1:def 1;
then ex x being Real st
( x = D1 . i & lower_bound A <= x & x <= upper_bound A ) ;
then lower_bound A in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } ;
hence lower_bound A in [.(lower_bound A),(D1 . i).] by RCOMP_1:def 1; :: thesis: verum
end;
D2 . j in [.(lower_bound A),(D1 . i).]
proof
A17: D2 . j in rng D2 by A2, FUNCT_1:def 5;
rng D2 c= A by INTEGRA1:def 2;
then A18: D2 . j in A by A17;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:5;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A18, RCOMP_1:def 1;
then ex x being Real st
( x = D2 . j & lower_bound A <= x & x <= upper_bound A ) ;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } by A8, A9;
hence D2 . j in [.(lower_bound A),(D1 . i).] by RCOMP_1:def 1; :: thesis: verum
end;
hence divset D2,j c= divset D1,i by A12, A13, A14, XXREAL_2:def 12; :: thesis: verum
end;
suppose A19: j <> 1 ; :: thesis: divset D2,j c= divset D1,i
then ( lower_bound (divset D2,j) = D2 . (j - 1) & upper_bound (divset D2,j) = D2 . j ) by A2, INTEGRA1:def 5;
then A20: divset D2,j = [.(D2 . (j - 1)),(D2 . j).] by INTEGRA1:5;
A21: D2 . (j - 1) in [.(lower_bound A),(D1 . i).]
proof
A22: j - 1 in dom D2 by A2, A19, INTEGRA1:9;
then A23: D2 . (j - 1) in rng D2 by FUNCT_1:def 5;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:5;
then A24: A = { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by RCOMP_1:def 1;
rng D2 c= A by INTEGRA1:def 2;
then D2 . (j - 1) in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A23, A24;
then A25: ex x being Real st
( x = D2 . (j - 1) & lower_bound A <= x & x <= upper_bound A ) ;
j <= j + 1 by NAT_1:11;
then j - 1 <= j by XREAL_1:22;
then D2 . (j - 1) <= D2 . j by A2, A22, GOBOARD2:18;
then ( lower_bound A <= D2 . (j - 1) & D2 . (j - 1) <= D1 . i ) by A8, A9, A25, XXREAL_0:2;
then D2 . (j - 1) in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } ;
hence D2 . (j - 1) in [.(lower_bound A),(D1 . i).] by RCOMP_1:def 1; :: thesis: verum
end;
D2 . j in [.(lower_bound A),(D1 . i).]
proof
A26: D2 . j in rng D2 by A2, FUNCT_1:def 5;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:5;
then A27: A = { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by RCOMP_1:def 1;
rng D2 c= A by INTEGRA1:def 2;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A26, A27;
then ex x being Real st
( x = D2 . j & lower_bound A <= x & x <= upper_bound A ) ;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } by A8, A9;
hence D2 . j in [.(lower_bound A),(D1 . i).] by RCOMP_1:def 1; :: thesis: verum
end;
hence divset D2,j c= divset D1,i by A12, A20, A21, XXREAL_2:def 12; :: thesis: verum
end;
end;
end;
hence divset D2,j c= divset D1,i ; :: thesis: verum
end;
suppose A28: i <> 1 ; :: thesis: divset D2,j c= divset D1,i
then ( lower_bound (divset D1,i) = D1 . (i - 1) & upper_bound (divset D1,i) = D1 . i ) by A9, INTEGRA1:def 5;
then A29: divset D1,i = [.(D1 . (i - 1)),(D1 . i).] by INTEGRA1:5;
A30: j <> 1
proof
assume A31: j = 1 ; :: thesis: contradiction
i in Seg (len D1) by A9, FINSEQ_1:def 3;
then A32: ( 1 <= i & i <= len D1 ) by FINSEQ_1:3;
then A33: i > 1 by A28, XXREAL_0:1;
( 1 <= 1 & 1 <= len D1 ) by A32, XXREAL_0:2;
then 1 in Seg (len D1) by FINSEQ_1:3;
then A34: 1 in dom D1 by FINSEQ_1:def 3;
then A35: D1 . 1 in rng D1 by FUNCT_1:def 5;
rng D1 c= rng D2 by A1, INTEGRA1:def 20;
then consider n being Element of NAT such that
A36: ( n in dom D2 & D1 . 1 = D2 . n ) by A35, PARTFUN1:26;
n in Seg (len D2) by A36, FINSEQ_1:def 3;
then A37: ( 1 <= n & n <= len D2 ) by FINSEQ_1:3;
then 1 <= len D2 by XXREAL_0:2;
then 1 in Seg (len D2) by FINSEQ_1:3;
then 1 in dom D2 by FINSEQ_1:def 3;
then D2 . j <= D2 . n by A31, A36, A37, GOBOARD2:18;
then n in X by A3, A35, A36;
then n >= min X by XXREAL_2:def 7;
then D1 . 1 >= D1 . i by A7, A9, A36, GOBOARD2:18;
hence contradiction by A9, A33, A34, SEQM_3:def 1; :: thesis: verum
end;
then ( lower_bound (divset D2,j) = D2 . (j - 1) & upper_bound (divset D2,j) = D2 . j ) by A2, INTEGRA1:def 5;
then A38: divset D2,j = [.(D2 . (j - 1)),(D2 . j).] by INTEGRA1:5;
A39: j - 1 in dom D2 by A2, A30, INTEGRA1:9;
j <= j + 1 by NAT_1:11;
then j - 1 <= j by XREAL_1:22;
then A40: D2 . (j - 1) <= D2 . j by A2, A39, GOBOARD2:18;
then A41: D2 . (j - 1) <= D1 . i by A10, XXREAL_0:2;
A42: D1 . (i - 1) <= D2 . (j - 1)
proof
assume A43: D1 . (i - 1) > D2 . (j - 1) ; :: thesis: contradiction
A44: rng D1 c= rng D2 by A1, INTEGRA1:def 20;
A45: i - 1 in dom D1 by A9, A28, INTEGRA1:9;
then A46: D1 . (i - 1) in rng D1 by FUNCT_1:def 5;
then consider n being Element of NAT such that
A47: ( n in dom D2 & D1 . (i - 1) = D2 . n ) by A44, PARTFUN1:26;
n > j - 1 by A39, A43, A47, GOBOARD2:18;
then n + 1 > j by XREAL_1:21;
then n >= j by NAT_1:13;
then D1 . (i - 1) >= D2 . j by A2, A47, GOBOARD2:18;
then n in X by A3, A46, A47;
then n >= min X by XXREAL_2:def 7;
then D1 . (i - 1) >= D1 . i by A7, A9, A47, GOBOARD2:18;
then i - 1 >= i by A9, A45, SEQM_3:def 1;
then A48: i >= i + 1 by XREAL_1:21;
i <= i + 1 by NAT_1:11;
then i = i + 1 by A48, XXREAL_0:1;
hence contradiction ; :: thesis: verum
end;
then D2 . (j - 1) in { r where r is Real : ( D1 . (i - 1) <= r & r <= D1 . i ) } by A41;
then A49: D2 . (j - 1) in [.(D1 . (i - 1)),(D1 . i).] by RCOMP_1:def 1;
( D1 . (i - 1) <= D2 . j & D2 . j <= D1 . i ) by A3, A7, A9, A40, A42, XXREAL_0:2;
then D2 . j in { r where r is Real : ( D1 . (i - 1) <= r & r <= D1 . i ) } ;
then D2 . j in [.(D1 . (i - 1)),(D1 . i).] by RCOMP_1:def 1;
hence divset D2,j c= divset D1,i by A29, A38, A49, XXREAL_2:def 12; :: thesis: verum
end;
end;
end;
hence divset D2,j c= divset D1,i ; :: thesis: verum
end;
take i ; :: thesis: ( i in dom D1 & divset D2,j c= divset D1,i )
thus ( i in dom D1 & divset D2,j c= divset D1,i ) by A9, A11; :: thesis: verum