let seq be Real_Sequence; :: thesis: ex f being Function of NAT ,REAL st
for n being Element of NAT
for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds
f . n = inf Y
defpred S₁[ Element of NAT , Element of REAL ] means for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : $1 <= k } holds
$2 = inf Y;
A1: for n being Element of NAT ex y being Element of REAL st S₁[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[n,y]
reconsider Y = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29;
reconsider y = lower_bound Y as Element of REAL ;
for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds
y = inf Y ;
hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

ex f being Function of NAT ,REAL st
for n being Element of NAT holds S₁[n,f . n] from FUNCT_2:sch 3(A1);
hence ex f being Function of NAT ,REAL st
for n being Element of NAT
for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds
f . n = inf Y ; :: thesis: verum