let A be Interval; :: thesis: J-Meas . A = diameter A
A1: A in Family_of_Intervals by MEASUR10:def 1;
A2: Family_of_Intervals c= Field_generated_by Family_of_Intervals by SRINGS_3:21;
reconsider F = <*A*> as disjoint_valued FinSequence of Family_of_Intervals by A1, FINSEQ_1:74;
rng F = {A} by FINSEQ_1:38;
then union (rng F) = A ;
then A = Union F by CARD_3:def 4;
then J-Meas . A = Sum (pre-Meas * F) by A2, A1, Def9;
then J-Meas . A = Sum <*(pre-Meas . A)*> by Th62;
then J-Meas . A = pre-Meas . A by EXTREAL1:8;
hence J-Meas . A = diameter A by Th59; :: thesis: verum