let A be 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
vol F1 = vol F2
let F1, F2 be 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 n, m be Nat; ( ( 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
; 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
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; verum