defpred S₁[ Element of NAT , set ] means $2 is middle_volume of f,T . $1;
A1: for x being Element of NAT ex y being Element of (REAL n) * st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of (REAL n) * st S₁[x,y]
consider y being middle_volume of f,T . x;
reconsider y = y as Element of (REAL n) * by FINSEQ_1:def 11;
y is middle_volume of f,T . x ;
hence ex y being Element of (REAL n) * st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of NAT ,((REAL n) * ) such that
A2: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 10(A1);
thus ex b₁ being Function of NAT ,((REAL n) * ) st
for k being Element of NAT holds b₁ . k is middle_volume of f,T . k by A2; :: thesis: verum