for A being Subset of REAL
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
for k being Nat st k >= n & k >= m holds
(Ser (F1 vol)) . k = (Ser (F2 vol)) . k