defpred S_{1}[ Element of NAT , Element of ExtREAL ] means $2 = SUM (vol (M,(Cvr . $1)));

A1: for n being Element of NAT ex y being Element of ExtREAL st S_{1}[n,y]
;

consider G0 being sequence of ExtREAL such that

A2: for n being Element of NAT holds S_{1}[n,G0 . n]
from FUNCT_2:sch 3(A1);

take G0 ; :: thesis: for n being Nat holds G0 . n = SUM (vol (M,(Cvr . n)))

A1: for n being Element of NAT ex y being Element of ExtREAL st S

consider G0 being sequence of ExtREAL such that

A2: for n being Element of NAT holds S

take G0 ; :: thesis: for n being Nat holds G0 . n = SUM (vol (M,(Cvr . n)))

hereby :: thesis: verum

let n be Nat; :: thesis: G0 . n = SUM (vol (M,(Cvr . n)))

n in NAT by ORDINAL1:def 12;

hence G0 . n = SUM (vol (M,(Cvr . n))) by A2; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence G0 . n = SUM (vol (M,(Cvr . n))) by A2; :: thesis: verum