let n, k be Nat; :: thesis: ( k in Seg (n + 1) implies divset ((EqDiv (['0,1'],(n + 1))),k) = [.((k -' 1) / (n + 1)),(k / (n + 1)).] )
set A = ['0,1'];
set D = EqDiv (['0,1'],(n + 1));
assume A1: k in Seg (n + 1) ; :: thesis: divset ((EqDiv (['0,1'],(n + 1))),k) = [.((k -' 1) / (n + 1)),(k / (n + 1)).]
A2: vol ['0,1'] = 1 - 0 by INTEGRA6:5;
then A3: EqDiv (['0,1'],(n + 1)) divide_into_equal n + 1 by MESFUN14:def 1;
then A4: len (EqDiv (['0,1'],(n + 1))) = n + 1 by INTEGRA4:def 1;
then A5: dom (EqDiv (['0,1'],(n + 1))) = Seg (n + 1) by FINSEQ_1:def 3;
A7: k in dom (EqDiv (['0,1'],(n + 1))) by A1, A4, FINSEQ_1:def 3;
A6: ( 1 <= k & k <= n + 1 ) by A1, FINSEQ_1:1;

per cases then ( k = 1 or k > 1 ) by XXREAL_0:1;

suppose A8: k = 1 ; :: thesis: divset ((EqDiv (['0,1'],(n + 1))),k) = [.((k -' 1) / (n + 1)),(k / (n + 1)).]

then [.((k -' 1) / (n + 1)),(k / (n + 1)).] = [.(0 / (n + 1)),(1 / (n + 1)).] by XREAL_1:232
.= [.0,(1 / (n + 1)).] ;
hence divset ((EqDiv (['0,1'],(n + 1))),k) = [.((k -' 1) / (n + 1)),(k / (n + 1)).] by A8, Lm1; :: thesis: verum

end;

suppose A9: k > 1 ; :: thesis: divset ((EqDiv (['0,1'],(n + 1))),k) = [.((k -' 1) / (n + 1)),(k / (n + 1)).]

then A10: k -' 1 = k - 1 by XREAL_1:233;
1 < (k - 1) + 1 by A9;
then A12: 1 <= k -' 1 by A10, NAT_1:13;
k -' 1 < k by A9, XREAL_1:237;
then k -' 1 < n + 1 by A6, XXREAL_0:2;
then A14: k -' 1 in dom (EqDiv (['0,1'],(n + 1))) by A12, A5;
k in dom (EqDiv (['0,1'],(n + 1))) by A1, A4, FINSEQ_1:def 3;
then A16: (EqDiv (['0,1'],(n + 1))) . k = (lower_bound ['0,1']) + (((vol ['0,1']) / (len (EqDiv (['0,1'],(n + 1))))) * k) by A3, INTEGRA4:def 1
.= 0 + ((1 / (n + 1)) * k) by FUZZY_6:7, A2, A4
.= k / (n + 1) ;
A17: (EqDiv (['0,1'],(n + 1))) . (k -' 1) = (lower_bound ['0,1']) + (((vol ['0,1']) / (len (EqDiv (['0,1'],(n + 1))))) * (k -' 1)) by A3, A14, INTEGRA4:def 1
.= 0 + ((1 / (n + 1)) * (k -' 1)) by FUZZY_6:7, A2, A4
.= (k -' 1) / (n + 1) ;
divset ((EqDiv (['0,1'],(n + 1))),k) = [.((EqDiv (['0,1'],(n + 1))) . (k - 1)),((EqDiv (['0,1'],(n + 1))) . k).] by A9, A7, COUSIN:50
.= [.((k -' 1) / (n + 1)),(k / (n + 1)).] by A9, XREAL_1:233, A16, A17 ;
hence divset ((EqDiv (['0,1'],(n + 1))),k) = [.((k -' 1) / (n + 1)),(k / (n + 1)).] ; :: thesis: verum

end;

end;