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) & len D = card (rng (D1 ^ D2)) & D is increasing ) by GOBOARD2:21;
reconsider D = D as increasing FinSequence of REAL by A1;
reconsider D = D as non empty increasing FinSequence of REAL by A1;
A2: rng (D1 ^ D2) = (rng D1) \/ (rng D2) by FINSEQ_1:44;
( rng D1 c= A & rng D2 c= A ) by INTEGRA1:def 2;
then A3: rng D c= A by A1, A2, XBOOLE_1:8;
A4: rng D1 c= rng (D1 ^ D2) by A2, XBOOLE_1:7;
A5: rng D2 c= rng (D1 ^ D2) by A2, XBOOLE_1:7;
D . (len D) = upper_bound A

proof

assume A6: D . (len D) <> upper_bound A ; :: thesis: contradiction
A7: 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 A3, INTEGRA2:1;
then A8: D . (len D) < upper_bound A by A6, XXREAL_0:1;
A9: D1 . (len D1) = upper_bound A by INTEGRA1:def 2;
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
A10: ( k in dom D & D1 . (len D1) = D . k ) by A1, A4, PARTFUN1:26;
k > len D by A7, A8, A9, A10, GOBOARD2:18;
hence contradiction by A10, FINSEQ_3:27; :: thesis: verum

end;

then reconsider D = D as Division of A by A3, INTEGRA1:def 2;
take D ; :: thesis: ( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )
A11: card (rng D1) <= len D by A1, A2, NAT_1:44, XBOOLE_1:7;
D1 is one-to-one by JORDAN7:17;
then len D1 <= len D by A11, FINSEQ_4:77;
hence D1 <= D by A1, A4, INTEGRA1:def 20; :: thesis: ( D2 <= D & rng D = (rng D1) \/ (rng D2) )
A12: card (rng D2) <= len D by A1, A2, NAT_1:44, XBOOLE_1:7;
D2 is one-to-one by JORDAN7:17;
then len D2 <= len D by A12, FINSEQ_4:77;
hence D2 <= D by A1, A5, INTEGRA1:def 20; :: thesis: rng D = (rng D1) \/ (rng D2)
thus rng D = (rng D1) \/ (rng D2) by A1, FINSEQ_1:44; :: thesis: verum