let A be 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:157;
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;
A6: rng (D1 ^ D2) = (rng D1) \/ (rng D2) by FINSEQ_1:44;
then A7: rng D1 c= rng (D1 ^ D2) by XBOOLE_1:7;
rng D1 c= A by INTEGRA1:def 2;
then A8: rng D c= A by A1, A6, A4, XBOOLE_1:8;
D . (len D) = upper_bound A

proof

len D1 in dom D1 by FINSEQ_5:6;
then D1 . (len D1) in rng D1 by FUNCT_1:def 5;
then consider k being Element of NAT such that
A9: k in dom D and
A10: D1 . (len D1) = D . k by A1, A7, PARTFUN1:26;
assume A11: D . (len D) <> upper_bound A ; :: thesis: contradiction
A12: len D in dom D by FINSEQ_5:6;
then D . (len D) in rng D by FUNCT_1:def 5;
then D . (len D) <= upper_bound A by A8, INTEGRA2:1;
then A13: D . (len D) < upper_bound A by A11, XXREAL_0:1;
D1 . (len D1) = upper_bound A by INTEGRA1:def 2;
then k > len D by A12, A13, A9, A10, SEQ_4:154;
hence contradiction by A9, FINSEQ_3:27; :: thesis: verum

end;

then reconsider D = D as Division of A by A8, INTEGRA1:def 2;
take D ; :: thesis: ( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )
card (rng D1) <= len D by A2, A6, NAT_1:44, XBOOLE_1:7;
then len D1 <= len D by FINSEQ_4:77;
hence D1 <= D by A1, A7, INTEGRA1:def 20; :: thesis: ( D2 <= D & rng D = (rng D1) \/ (rng D2) )
A15: rng D2 c= rng (D1 ^ D2) by A6, XBOOLE_1:7;
card (rng D2) <= len D by A2, A6, NAT_1:44, XBOOLE_1:7;
then len D2 <= len D by FINSEQ_4:77;
hence D2 <= D by A1, A15, INTEGRA1:def 20; :: thesis: rng D = (rng D1) \/ (rng D2)
thus rng D = (rng D1) \/ (rng D2) by A1, FINSEQ_1:44; :: thesis: verum