let Iac, Icb, I be non empty closed_interval Subset of REAL; :: thesis: for D1 being Division of Iac
for D2 being Division of Icb st upper_bound Iac <= lower_bound Icb & I = [.(lower_bound Iac),(upper_bound Icb).] holds
D1 (#) D2 is Division of I
let Dac be Division of Iac; :: thesis: for D2 being Division of Icb st upper_bound Iac <= lower_bound Icb & I = [.(lower_bound Iac),(upper_bound Icb).] holds
Dac (#) D2 is Division of I
let Dcb be Division of Icb; :: thesis: ( upper_bound Iac <= lower_bound Icb & I = [.(lower_bound Iac),(upper_bound Icb).] implies Dac (#) Dcb is Division of I )
assume that
A1: upper_bound Iac <= lower_bound Icb and
A2: I = [.(lower_bound Iac),(upper_bound Icb).] ; :: thesis: Dac (#) Dcb is Division of I
lower_bound Iac <= upper_bound Iac by BORSUK_4:28;
then A3: lower_bound Iac <= lower_bound Icb by A1, XXREAL_0:2;
lower_bound Icb <= upper_bound Icb by BORSUK_4:28;
then A4: lower_bound Iac <= upper_bound Icb by A3, XXREAL_0:2;
then ( lower_bound I = lower_bound Iac & upper_bound I = upper_bound Icb ) by A2, JORDAN5A:19;
then A5: Iac \/ Icb c= I by A1, Th37;
A6: rng Dac c= Iac by INTEGRA1:def 2;
A7: rng Dcb c= Icb by INTEGRA1:def 2;
rng Dcb <> {} ;
then 1 in dom Dcb by FINSEQ_3:32;
then A8: 1 in Seg (len Dcb) by FINSEQ_1:def 3;
then 1 <= len Dcb by FINSEQ_1:1;
then A9: (len Dac) + 1 <= (len Dac) + (len Dcb) by XREAL_1:7;
set Dacb = Dac (#) Dcb;

per cases ( Dcb . 1 <> upper_bound Iac or Dcb . 1 = upper_bound Iac ) ;

suppose Dcb . 1 <> upper_bound Iac ; :: thesis: Dac (#) Dcb is Division of I

then A10: Dac (#) Dcb = Dac ^ Dcb by A1, Def4;
rng (Dac (#) Dcb) = (rng Dac) \/ (rng Dcb) by A10, FINSEQ_1:31;
then rng (Dac (#) Dcb) c= Iac \/ Icb by A6, A7, XBOOLE_1:13;
then A11: rng (Dac (#) Dcb) c= I by A5;
len (Dac (#) Dcb) = (len Dac) + (len Dcb) by A10, FINSEQ_1:22;
then (Dac (#) Dcb) . (len (Dac (#) Dcb)) = Dcb . (((len Dac) + (len Dcb)) - (len Dac)) by A9, A10, FINSEQ_1:23
.= upper_bound Icb by INTEGRA1:def 2
.= upper_bound I by A4, A2, JORDAN5A:19 ;
hence Dac (#) Dcb is Division of I by A11, INTEGRA1:def 2; :: thesis: verum

end;

suppose A12: Dcb . 1 = upper_bound Iac ; :: thesis: Dac (#) Dcb is Division of I

then A13: Dac (#) Dcb = Dac ^ (Dcb /^ 1) by A1, Def4;
then A14: rng (Dac (#) Dcb) c= (rng Dac) \/ (rng (Dcb /^ 1)) by FINSEQ_1:31;
rng (Dcb /^ 1) c= rng Dcb by FINSEQ_5:33;
then A15: (rng Dac) \/ (rng (Dcb /^ 1)) c= (rng Dac) \/ (rng Dcb) by XBOOLE_1:13;
(rng Dac) \/ (rng Dcb) c= Iac \/ Icb by A6, A7, XBOOLE_1:13;
then rng (Dac (#) Dcb) c= Iac \/ Icb by A14, A15;
then A16: rng (Dac (#) Dcb) c= I by A5;
A17: len (Dac (#) Dcb) = (len Dac) + (len (Dcb /^ 1)) by A13, FINSEQ_1:22;
A18: 1 <= len Dcb by A8, FINSEQ_1:1;
then A18bis: len (Dcb /^ 1) = (len Dcb) - 1 by RFINSEQ:def 1;

per cases ( len Dcb = 1 or len Dcb <> 1 ) ;

suppose A19: len Dcb = 1 ; :: thesis: Dac (#) Dcb is Division of I

then Dcb /^ 1 is empty by FINSEQ_5:32;
then Dac (#) Dcb = Dac by A13, FINSEQ_1:34;
then (Dac (#) Dcb) . (len (Dac (#) Dcb)) = Dcb . (len Dcb) by A12, A19, INTEGRA1:def 2
.= upper_bound Icb by INTEGRA1:def 2
.= upper_bound I by A4, A2, JORDAN5A:19 ;
hence Dac (#) Dcb is Division of I by A16, INTEGRA1:def 2; :: thesis: verum

end;

suppose len Dcb <> 1 ; :: thesis: Dac (#) Dcb is Division of I

then A20: 2 - 1 <= (len Dcb) - 1 by NAT_1:23, XREAL_1:9;
A21: Seg (len (Dcb /^ 1)) = dom (Dcb /^ 1) by FINSEQ_1:def 3;
A22: len (Dcb /^ 1) = (len Dcb) - 1 by A18, RFINSEQ:def 1;
1 <= len (Dcb /^ 1) by A18, RFINSEQ:def 1, A20;
then A23: len (Dcb /^ 1) in dom (Dcb /^ 1) by A21, FINSEQ_1:1;
Dcb /^ 1 <> {} by A22, A20;
then rng (Dcb /^ 1) <> {} ;
then 1 in dom (Dcb /^ 1) by FINSEQ_3:32;
then 1 <= len (Dcb /^ 1) by FINSEQ_3:25;
then ( (len Dac) + 1 <= (len Dac) + (len (Dcb /^ 1)) & (len Dac) + (len (Dcb /^ 1)) <= (len Dac) + (len (Dcb /^ 1)) ) by XREAL_1:7;
then (Dac (#) Dcb) . (len (Dac (#) Dcb)) = (Dcb /^ 1) . (((len Dac) + (len (Dcb /^ 1))) - (len Dac)) by A17, A13, FINSEQ_1:23
.= Dcb . ((len (Dcb /^ 1)) + 1) by A18, RFINSEQ:def 1, A23
.= upper_bound Icb by A18bis, INTEGRA1:def 2
.= upper_bound I by A4, A2, JORDAN5A:19 ;
hence Dac (#) Dcb is Division of I by A16, INTEGRA1:def 2; :: thesis: verum

end;

end;

end;

end;