let a, b be Real; :: thesis: for Iab being non empty compact Subset of REAL
for Dab being Division of Iab st 2 <= len Dab holds
Dab /^ 1 is Division of Iab
let Iab be non empty compact Subset of REAL; :: thesis: for Dab being Division of Iab st 2 <= len Dab holds
Dab /^ 1 is Division of Iab
let Dab be Division of Iab; :: thesis: ( 2 <= len Dab implies Dab /^ 1 is Division of Iab )
assume A1: 2 <= len Dab ; :: thesis: Dab /^ 1 is Division of Iab
set D = Dab /^ 1;
A2: 1 <= len Dab by A1, XXREAL_0:2;
then A3: len (Dab /^ 1) = (len Dab) - 1 by RFINSEQ:def 1;
A5: not Dab /^ 1 is empty

proof

2 - 1 <= (len Dab) - 1 by A1, XREAL_1:13;
hence not Dab /^ 1 is empty by A3; :: thesis: verum

end;

A4: ( not Dab /^ 1 is empty & Dab /^ 1 is increasing )

proof

Dab /^ 1 is increasing

proof

now :: thesis: for e1, e2 being ExtReal st e1 in dom (Dab /^ 1) & e2 in dom (Dab /^ 1) & e1 < e2 holds
(Dab /^ 1) . e1 < (Dab /^ 1) . e2

let e1, e2 be ExtReal; :: thesis: ( e1 in dom (Dab /^ 1) & e2 in dom (Dab /^ 1) & e1 < e2 implies (Dab /^ 1) . e1 < (Dab /^ 1) . e2 )
assume that
A6: e1 in dom (Dab /^ 1) and
A7: e2 in dom (Dab /^ 1) and
A8: e1 < e2 ; :: thesis: (Dab /^ 1) . e1 < (Dab /^ 1) . e2
reconsider ne1 = e1, ne2 = e2 as Nat by A6, A7;
A9: (Dab /^ 1) . e1 = Dab . (ne1 + 1) by A2, A6, RFINSEQ:def 1;
ne1 in Seg (len (Dab /^ 1)) by A6, FINSEQ_1:def 3;
then ne1 + 1 in Seg ((len (Dab /^ 1)) + 1) by FINSEQ_1:60;
then A10: ne1 + 1 in dom Dab by A3, FINSEQ_1:def 3;
( ne2 in Seg (len (Dab /^ 1)) & ne2 in Seg (len (Dab /^ 1)) ) by A7, FINSEQ_1:def 3;
then ne2 + 1 in Seg ((len (Dab /^ 1)) + 1) by FINSEQ_1:60;
then A11: ne2 + 1 in dom Dab by A3, FINSEQ_1:def 3;
A12: (Dab /^ 1) . e2 = Dab . (ne2 + 1) by A2, A7, RFINSEQ:def 1;
ne1 + 1 < ne2 + 1 by A8, XREAL_1:8;
hence (Dab /^ 1) . e1 < (Dab /^ 1) . e2 by A9, A12, A10, A11, VALUED_0:def 13; :: thesis: verum

end;

hence Dab /^ 1 is increasing ; :: thesis: verum

end;

hence ( not Dab /^ 1 is empty & Dab /^ 1 is increasing ) by A5; :: thesis: verum

end;

A13: rng (Dab /^ 1) c= Iab

proof

A14: rng (Dab /^ 1) c= rng Dab by FINSEQ_5:33;
rng Dab c= Iab by INTEGRA1:def 2;
hence rng (Dab /^ 1) c= Iab by A14; :: thesis: verum

end;

(Dab /^ 1) . (len (Dab /^ 1)) = upper_bound Iab

proof

2 - 1 <= (len Dab) - 1 by A1, XREAL_1:13;
then ( Seg (len (Dab /^ 1)) = dom (Dab /^ 1) & len (Dab /^ 1) in Seg (len (Dab /^ 1)) ) by A3, FINSEQ_1:def 3, FINSEQ_1:3;
then (Dab /^ 1) . (len (Dab /^ 1)) = Dab . ((len (Dab /^ 1)) + 1) by A2, RFINSEQ:def 1
.= Dab . (len Dab) by A3 ;
hence (Dab /^ 1) . (len (Dab /^ 1)) = upper_bound Iab by INTEGRA1:def 2; :: thesis: verum

end;

hence Dab /^ 1 is Division of Iab by A4, A13, INTEGRA1:def 2; :: thesis: verum