defpred S₁[ Element of NAT , Element of REAL ] means for Y being Subset of REAL st Y = { (seq . k) where k is Nat : $1 <= k } holds
$2 = upper_bound 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 Nat : n <= k } as Subset of REAL by Th29;
reconsider y = upper_bound Y as Element of REAL by XREAL_0:def 1;
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
y = upper_bound Y ;
hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

consider f being sequence of REAL such that
A2: for n being Element of NAT holds S₁[n,f . n] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
f . n = upper_bound Y
let n be Nat; :: thesis: for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
f . n = upper_bound Y
n in NAT by ORDINAL1:def 12;
hence for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
f . n = upper_bound Y by A2; :: thesis: verum