defpred S₁[ Element of NAT , set ] means $2 = (G . $1) vol ;
A1: for n being Element of NAT ex y being Element of Funcs (NAT,ExtREAL) st S₁[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of Funcs (NAT,ExtREAL) st S₁[n,y]
(G . n) vol is Element of Funcs (NAT,ExtREAL) by FUNCT_2:8;
hence ex y being Element of Funcs (NAT,ExtREAL) st S₁[n,y] ; :: thesis: verum

end;

ex G0 being Function of NAT,(Funcs (NAT,ExtREAL)) st
for n being Element of NAT holds S₁[n,G0 . n] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of NAT,(Funcs (NAT,ExtREAL)) st
for n being Element of NAT holds b₁ . n = (G . n) vol ; :: thesis: verum