let a, b, c be Real; :: thesis: for Iab, Iac, Icb being non empty compact Subset of REAL st a <= c & c <= b & Iab = [.a,b.] & Iac = [.a,c.] & Icb = [.c,b.] holds
for Dac being Division of Iac
for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab
let Iab, Iac, Icb be non empty compact Subset of REAL; :: thesis: ( a <= c & c <= b & Iab = [.a,b.] & Iac = [.a,c.] & Icb = [.c,b.] implies for Dac being Division of Iac
for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab )
assume that
A1: ( a <= c & c <= b ) and
A2: Iab = [.a,b.] and
A3: Iac = [.a,c.] and
A4: Icb = [.c,b.] ; :: thesis: for Dac being Division of Iac
for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab
let Dac be Division of Iac; :: thesis: for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab
let Dcb be Division of Icb; :: thesis: ( c < Dcb . 1 implies Dac ^ Dcb is Division of Iab )
assume A5: c < Dcb . 1 ; :: thesis: Dac ^ Dcb is Division of Iab
set Dacb = Dac ^ Dcb;
for e1, e2 being ExtReal st e1 in dom (Dac ^ Dcb) & e2 in dom (Dac ^ Dcb) & e1 < e2 holds
(Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2

proof

let e1, e2 be ExtReal; :: thesis: ( e1 in dom (Dac ^ Dcb) & e2 in dom (Dac ^ Dcb) & e1 < e2 implies (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2 )
assume that
A6: e1 in dom (Dac ^ Dcb) and
A7: e2 in dom (Dac ^ Dcb) and
A8: e1 < e2 ; :: thesis: (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2

per cases ( ( e1 in dom Dac & e2 in dom Dac ) or ( e1 in dom Dac & ex n being Nat st
( n in dom Dcb & e2 = (len Dac) + n ) ) or ( ex n being Nat st
( n in dom Dcb & e1 = (len Dac) + n ) & e2 in dom Dac ) or ( ex n being Nat st
( n in dom Dcb & e1 = (len Dac) + n ) & ex n being Nat st
( n in dom Dcb & e2 = (len Dac) + n ) ) ) by A6, A7, FINSEQ_1:25;

suppose A9: ( e1 in dom Dac & e2 in dom Dac ) ; :: thesis: (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2

then A10: ( (Dac ^ Dcb) . e1 = Dac . e1 & (Dac ^ Dcb) . e2 = Dac . e2 ) by FINSEQ_1:def 7;
( e1 < e2 & Dac is increasing ) by A8;
hence (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2 by A9, A10; :: thesis: verum

end;

suppose A11: ( e1 in dom Dac & ex n being Nat st
( n in dom Dcb & e2 = (len Dac) + n ) ) ; :: thesis: (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2

then consider n0 being Nat such that
A12: n0 in dom Dcb and
A13: e2 = (len Dac) + n0 ;
( (Dac ^ Dcb) . e1 = Dac . e1 & (Dac ^ Dcb) . e2 = Dcb . n0 ) by A11, A13, FINSEQ_1:def 7;
hence (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2 by A11, A12, A3, A4, A5, Th44, A1; :: thesis: verum

end;

suppose A14: ( ex n being Nat st
( n in dom Dcb & e1 = (len Dac) + n ) & e2 in dom Dac ) ; :: thesis: (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2

then consider n0 being Nat such that
n0 in dom Dcb and
A15: e1 = (len Dac) + n0 ;
A16: len Dac <= e1 by A15, NAT_1:11;
e2 in Seg (len Dac) by FINSEQ_1:def 3, A14;
then e2 <= len Dac by FINSEQ_1:1;
hence (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2 by A8, A16, XXREAL_0:2; :: thesis: verum

end;

suppose A17: ( ex n being Nat st
( n in dom Dcb & e1 = (len Dac) + n ) & ex n being Nat st
( n in dom Dcb & e2 = (len Dac) + n ) ) ; :: thesis: (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2

then consider n1 being Nat such that
A18: n1 in dom Dcb and
A19: e1 = (len Dac) + n1 ;
consider n2 being Nat such that
A20: n2 in dom Dcb and
A21: e2 = (len Dac) + n2 by A17;
A22: ((len Dac) + n1) - (len Dac) < ((len Dac) + n2) - (len Dac) by A8, A19, A21, XREAL_1:14;
( Dcb . n1 = (Dac ^ Dcb) . e1 & Dcb . n2 = (Dac ^ Dcb) . e2 ) by A17, A19, A21, FINSEQ_1:def 7;
hence (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2 by A22, A18, A20, VALUED_0:def 13; :: thesis: verum

end;

end;

end;

then A23: Dac ^ Dcb is increasing ;
A24: rng (Dac ^ Dcb) c= Iab

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Dac ^ Dcb) or x in Iab )
assume A25: x in rng (Dac ^ Dcb) ; :: thesis: x in Iab
A26: rng Dac c= [.a,c.] by A3, INTEGRA1:def 2;
rng Dcb c= [.c,b.] by A4, INTEGRA1:def 2;
then (rng Dac) \/ (rng Dcb) c= [.a,c.] \/ [.c,b.] by XBOOLE_1:13, A26;
then rng (Dac ^ Dcb) c= [.a,c.] \/ [.c,b.] by FINSEQ_1:31;
then rng (Dac ^ Dcb) c= [.a,b.] by A1, XXREAL_1:165;
hence x in Iab by A25, A2; :: thesis: verum

end;

(Dac ^ Dcb) . (len (Dac ^ Dcb)) = upper_bound Iab

proof

A27: a <= b by A1, XXREAL_0:2;
A28: len Dcb in Seg (len Dcb) by FINSEQ_1:3;
A29: Seg (len Dcb) = dom Dcb by FINSEQ_1:def 3;
len (Dac ^ Dcb) = (len Dac) + (len Dcb) by FINSEQ_1:22;
then (Dac ^ Dcb) . (len (Dac ^ Dcb)) = Dcb . (len Dcb) by A29, A28, FINSEQ_1:def 7
.= upper_bound Icb by INTEGRA1:def 2
.= b by JORDAN5A:19, A1, A4
.= upper_bound [.a,b.] by A27, JORDAN5A:19 ;
hence (Dac ^ Dcb) . (len (Dac ^ Dcb)) = upper_bound Iab by A2; :: thesis: verum

end;

hence Dac ^ Dcb is Division of Iab by A23, A24, INTEGRA1:def 2; :: thesis: verum