defpred S₁[ 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₁[n,y] ;
consider G0 being Function of NAT,ExtREAL such that
A2: for n being Element of NAT holds S₁[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;