let A, B be Subset of REAL; :: thesis: for F being Interval_Covering of A
for G being Interval_Covering of B st F = G holds
F vol = G vol
let F be Interval_Covering of A; :: thesis: for G being Interval_Covering of B st F = G holds
F vol = G vol
let G be Interval_Covering of B; :: thesis: ( F = G implies F vol = G vol )
assume A1: F = G ; :: thesis: F vol = G vol
for n being Element of NAT holds (F vol) . n = (G vol) . n

proof

let n be Element of NAT ; :: thesis: (F vol) . n = (G vol) . n
(F vol) . n = diameter (F . n) by MEASURE7:def 4;
hence (F vol) . n = (G vol) . n by A1, MEASURE7:def 4; :: thesis: verum

end;

hence F vol = G vol by FUNCT_2:def 8; :: thesis: verum