let A be Subset of REAL; :: thesis: for F1, F2 being Interval_Covering of A
for n, m being Nat st ( for k being Nat st k <> n & k <> m holds
F1 . k = F2 . k ) & F1 . n = F2 . m & F1 . m = F2 . n holds
vol F1 = vol F2
let F1, F2 be Interval_Covering of A; :: thesis: for n, m being Nat st ( for k being Nat st k <> n & k <> m holds
F1 . k = F2 . k ) & F1 . n = F2 . m & F1 . m = F2 . n holds
vol F1 = vol F2
let n, m be Nat; :: thesis: ( ( for k being Nat st k <> n & k <> m holds
F1 . k = F2 . k ) & F1 . n = F2 . m & F1 . m = F2 . n implies vol F1 = vol F2 )
assume that
A1: for k being Nat st k <> n & k <> m holds
F1 . k = F2 . k and
A2: F1 . n = F2 . m and
A3: F1 . m = F2 . n ; :: thesis: vol F1 = vol F2
A4: ( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;
then ( (F1 vol) . n = diameter (F1 . n) & (F1 vol) . m = diameter (F1 . m) ) by MEASURE7:def 4;
then A5: ( (F1 vol) . n = (F2 vol) . m & (F1 vol) . m = (F2 vol) . n ) by A2, A3, A4, MEASURE7:def 4;
A6: for k being Nat st k <> n & k <> m holds
(F1 vol) . k = (F2 vol) . k

proof

let k be Nat; :: thesis: ( k <> n & k <> m implies (F1 vol) . k = (F2 vol) . k )
A7: k is Element of NAT by ORDINAL1:def 12;
assume ( k <> n & k <> m ) ; :: thesis: (F1 vol) . k = (F2 vol) . k
then F1 . k = F2 . k by A1;
then (F1 vol) . k = diameter (F2 . k) by A7, MEASURE7:def 4;
hence (F1 vol) . k = (F2 vol) . k by A7, MEASURE7:def 4; :: thesis: verum

end;

then A8: for k being Nat st k <> m & k <> n holds
(F2 vol) . k = (F1 vol) . k ;
( n >= m or m > n ) ;
then SUM (F1 vol) = SUM (F2 vol) by A5, A6, A8, Th51, MEASURE7:12;
then vol F1 = SUM (F2 vol) by MEASURE7:def 6;
hence vol F1 = vol F2 by MEASURE7:def 6; :: thesis: verum