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

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

hence
G1 = G2
by FUNCT_2:12; :: thesis: verumG1 . 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;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