let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A st D1 <= D2 holds
indx (D2,D1,(len D1)) = len D2
let D1, D2 be Division of A; :: thesis: ( D1 <= D2 implies indx (D2,D1,(len D1)) = len D2 )
len D1 in Seg (len D1) by FINSEQ_1:3;
then A1: len D1 in dom D1 by FINSEQ_1:def 3;
assume A2: D1 <= D2 ; :: thesis: indx (D2,D1,(len D1)) = len D2
then D1 . (len D1) = D2 . (indx (D2,D1,(len D1))) by A1, Def18;
then A3: D2 . (indx (D2,D1,(len D1))) = upper_bound A by Def1;
len D2 in Seg (len D2) by FINSEQ_1:3;
then A4: len D2 in dom D2 by FINSEQ_1:def 3;
assume A5: indx (D2,D1,(len D1)) <> len D2 ; :: thesis: contradiction
A6: indx (D2,D1,(len D1)) in dom D2 by A2, A1, Def18;
then indx (D2,D1,(len D1)) in Seg (len D2) by FINSEQ_1:def 3;
then indx (D2,D1,(len D1)) <= len D2 by FINSEQ_1:1;
then indx (D2,D1,(len D1)) < len D2 by A5, XXREAL_0:1;
then D2 . (indx (D2,D1,(len D1))) < D2 . (len D2) by A4, A6, SEQM_3:def 1;
hence contradiction by A3, Def1; :: thesis: verum