let G1, G2 be sequence of ExtREAL; :: thesis: ( ( for n being Nat holds G1 . n = SUM (vol (M,(Cvr . n))) ) & ( for n being Nat holds G2 . n = SUM (vol (M,(Cvr . n))) ) implies G1 = G2 )
assume that
A3: for n being Nat holds G1 . n = SUM (vol (M,(Cvr . n))) and
A4: for n being Nat holds G2 . n = SUM (vol (M,(Cvr . n))) ; :: thesis: G1 = G2

now :: thesis: for x being object st x in NAT holds
G1 . x = G2 . x

let x be object ; :: thesis: ( x in NAT implies G1 . x = G2 . x )
assume x in NAT ; :: thesis: G1 . x = G2 . x
then reconsider n = x as Nat ;
thus G1 . x = SUM (vol (M,(Cvr . n))) by A3
.= G2 . x by A4 ; :: thesis: verum

end;

hence G1 = G2 by FUNCT_2:12; :: thesis: verum