defpred S₁[ Element of NAT , Element of ExtREAL ] means $2 = vol (G . $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 Element of NAT holds G0 . n = vol (G . n)
thus for n being Element of NAT holds G0 . n = vol (G . n) by A2; :: thesis: verum