defpred S_{1}[ Element of NAT , set ] means $2 is middle_volume of rho,u,T . $1;

A1: for x being Element of NAT ex y being Element of REAL * st S_{1}[x,y]

for x being Element of NAT holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

hence ex b_{1} being sequence of (REAL *) st

for k being Element of NAT holds b_{1} . k is middle_volume of rho,u,T . k
; :: thesis: verum

A1: for x being Element of NAT ex y being Element of REAL * st S

proof

ex f being sequence of (REAL *) st
let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S_{1}[x,y]

set y = the middle_volume of rho,u,T . x;

reconsider y = the middle_volume of rho,u,T . x as Element of REAL * by FINSEQ_1:def 11;

y is middle_volume of rho,u,T . x ;

hence ex y being Element of REAL * st S_{1}[x,y]
; :: thesis: verum

end;set y = the middle_volume of rho,u,T . x;

reconsider y = the middle_volume of rho,u,T . x as Element of REAL * by FINSEQ_1:def 11;

y is middle_volume of rho,u,T . x ;

hence ex y being Element of REAL * st S

for x being Element of NAT holds S

hence ex b

for k being Element of NAT holds b