let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A ex D being Division of A st

( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )

let D1, D2 be Division of A; :: thesis: ex D being Division of A st

( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )

consider D being FinSequence of REAL such that

A1: rng D = rng (D1 ^ D2) and

A2: len D = card (rng (D1 ^ D2)) and

A3: D is increasing by SEQ_4:140;

reconsider D = D as increasing FinSequence of REAL by A3;

reconsider D = D as non empty increasing FinSequence of REAL by A1;

A4: rng D2 c= A by INTEGRA1:def 2;

A5: rng (D1 ^ D2) = (rng D1) \/ (rng D2) by FINSEQ_1:31;

then A6: rng D1 c= rng (D1 ^ D2) by XBOOLE_1:7;

rng D1 c= A by INTEGRA1:def 2;

then A7: rng D c= A by A1, A5, A4, XBOOLE_1:8;

D . (len D) = upper_bound A

take D ; :: thesis: ( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )

card (rng D1) <= len D by A2, A5, NAT_1:43, XBOOLE_1:7;

then len D1 <= len D by FINSEQ_4:62;

hence D1 <= D by A1, A6, INTEGRA1:def 18; :: thesis: ( D2 <= D & rng D = (rng D1) \/ (rng D2) )

A13: rng D2 c= rng (D1 ^ D2) by A5, XBOOLE_1:7;

card (rng D2) <= len D by A2, A5, NAT_1:43, XBOOLE_1:7;

then len D2 <= len D by FINSEQ_4:62;

hence D2 <= D by A1, A13, INTEGRA1:def 18; :: thesis: rng D = (rng D1) \/ (rng D2)

thus rng D = (rng D1) \/ (rng D2) by A1, FINSEQ_1:31; :: thesis: verum

( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )

let D1, D2 be Division of A; :: thesis: ex D being Division of A st

( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )

consider D being FinSequence of REAL such that

A1: rng D = rng (D1 ^ D2) and

A2: len D = card (rng (D1 ^ D2)) and

A3: D is increasing by SEQ_4:140;

reconsider D = D as increasing FinSequence of REAL by A3;

reconsider D = D as non empty increasing FinSequence of REAL by A1;

A4: rng D2 c= A by INTEGRA1:def 2;

A5: rng (D1 ^ D2) = (rng D1) \/ (rng D2) by FINSEQ_1:31;

then A6: rng D1 c= rng (D1 ^ D2) by XBOOLE_1:7;

rng D1 c= A by INTEGRA1:def 2;

then A7: rng D c= A by A1, A5, A4, XBOOLE_1:8;

D . (len D) = upper_bound A

proof

then reconsider D = D as Division of A by A7, INTEGRA1:def 2;
len D1 in dom D1
by FINSEQ_5:6;

then D1 . (len D1) in rng D1 by FUNCT_1:def 3;

then consider k being Element of NAT such that

A8: k in dom D and

A9: D1 . (len D1) = D . k by A1, A6, PARTFUN1:3;

assume A10: D . (len D) <> upper_bound A ; :: thesis: contradiction

A11: len D in dom D by FINSEQ_5:6;

then D . (len D) in rng D by FUNCT_1:def 3;

then D . (len D) <= upper_bound A by A7, INTEGRA2:1;

then A12: D . (len D) < upper_bound A by A10, XXREAL_0:1;

D1 . (len D1) = upper_bound A by INTEGRA1:def 2;

then k > len D by A11, A12, A8, A9, SEQ_4:137;

hence contradiction by A8, FINSEQ_3:25; :: thesis: verum

end;then D1 . (len D1) in rng D1 by FUNCT_1:def 3;

then consider k being Element of NAT such that

A8: k in dom D and

A9: D1 . (len D1) = D . k by A1, A6, PARTFUN1:3;

assume A10: D . (len D) <> upper_bound A ; :: thesis: contradiction

A11: len D in dom D by FINSEQ_5:6;

then D . (len D) in rng D by FUNCT_1:def 3;

then D . (len D) <= upper_bound A by A7, INTEGRA2:1;

then A12: D . (len D) < upper_bound A by A10, XXREAL_0:1;

D1 . (len D1) = upper_bound A by INTEGRA1:def 2;

then k > len D by A11, A12, A8, A9, SEQ_4:137;

hence contradiction by A8, FINSEQ_3:25; :: thesis: verum

take D ; :: thesis: ( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )

card (rng D1) <= len D by A2, A5, NAT_1:43, XBOOLE_1:7;

then len D1 <= len D by FINSEQ_4:62;

hence D1 <= D by A1, A6, INTEGRA1:def 18; :: thesis: ( D2 <= D & rng D = (rng D1) \/ (rng D2) )

A13: rng D2 c= rng (D1 ^ D2) by A5, XBOOLE_1:7;

card (rng D2) <= len D by A2, A5, NAT_1:43, XBOOLE_1:7;

then len D2 <= len D by FINSEQ_4:62;

hence D2 <= D by A1, A13, INTEGRA1:def 18; :: thesis: rng D = (rng D1) \/ (rng D2)

thus rng D = (rng D1) \/ (rng D2) by A1, FINSEQ_1:31; :: thesis: verum