let G1, G2 be Function of NAT ,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

let x be set ; :: 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:18; :: thesis: verum