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
for k being Nat st k >= n & k >= m holds
(Ser (F1 vol)) . k = (Ser (F2 vol)) . k
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
for k being Nat st k >= n & k >= m holds
(Ser (F1 vol)) . k = (Ser (F2 vol)) . k
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 for k being Nat st k >= n & k >= m holds
(Ser (F1 vol)) . k = (Ser (F2 vol)) . k )
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: for k being Nat st k >= n & k >= m holds
(Ser (F1 vol)) . k = (Ser (F2 vol)) . k
let k be Nat; :: thesis: ( k >= n & k >= m implies (Ser (F1 vol)) . k = (Ser (F2 vol)) . k )
assume that
A4: k >= n and
A5: k >= m ; :: thesis: (Ser (F1 vol)) . k = (Ser (F2 vol)) . k
A6: ( 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 A7: ( (F1 vol) . n = (F2 vol) . m & (F1 vol) . m = (F2 vol) . n ) by A2, A3, A6, MEASURE7:def 4;
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 )
A8: 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 A8, MEASURE7:def 4;
hence (F1 vol) . k = (F2 vol) . k by A8, MEASURE7:def 4; :: thesis: verum
end;
hence (Ser (F1 vol)) . k = (Ser (F2 vol)) . k by A4, A5, A7, Th50, MEASURE7:12; :: thesis: verum