defpred S1[ 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 S1[n,y] ;
consider G0 being sequence of ExtREAL such that
A2: for n being Element of NAT holds S1[n,G0 . n] from FUNCT_2:sch 3(A1);
 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;