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 the carrier of X * st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of the carrier of X * st S₁[x,y]
set y = the middle_volume of f,T . x;
reconsider y = the middle_volume of f,T . x as Element of the carrier of X * by FINSEQ_1:def 11;
y is middle_volume of f,T . x ;
hence ex y being Element of the carrier of X * st S₁[x,y] ; :: thesis: verum

end;

ex f being sequence of ( the carrier of X *) st
for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being sequence of ( the carrier of X *) st
for k being Element of NAT holds b₁ . k is middle_volume of f,T . k ; :: thesis: verum