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 ;
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 3;
then consider k being Element of NAT such that
A8: k in dom D and
A9: D1 . (len D1) = D . k by ;
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 ;
then A12: D . (len D) < upper_bound A by ;
D1 . (len D1) = upper_bound A by INTEGRA1:def 2;
then k > len D by ;
hence contradiction by A8, FINSEQ_3:25; :: thesis: verum
end;
then reconsider D = D as Division of A by ;
take D ; :: thesis: ( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )
card (rng D1) <= len D by ;
then len D1 <= len D by FINSEQ_4:62;
hence D1 <= D by ; :: thesis: ( D2 <= D & rng D = (rng D1) \/ (rng D2) )
A13: rng D2 c= rng (D1 ^ D2) by ;
card (rng D2) <= len D by ;
then len D2 <= len D by FINSEQ_4:62;
hence D2 <= D by ; :: thesis: rng D = (rng D1) \/ (rng D2)
thus rng D = (rng D1) \/ (rng D2) by ; :: thesis: verum