defpred S₁[ Nat, Element of ExtREAL ] means ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : $1 <= k } & $2 = inf Y );
A1: for n being Element of NAT ex y being Element of ExtREAL st S₁[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of ExtREAL st S₁[n,y]
reconsider Y = { (seq . k) where k is Nat : n <= k } as non empty Subset of ExtREAL by Th5;
reconsider y = inf Y as Element of ExtREAL ;
take y ; :: thesis: S₁[n,y]
thus S₁[n,y] ; :: thesis: verum

end;

consider f being sequence of ExtREAL 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 ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : n <= k } & f . n = inf Y )
let n be Nat; :: thesis: ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : n <= k } & f . n = inf Y )
n in NAT by ORDINAL1:def 12;
hence ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : n <= k } & f . n = inf Y ) by A2; :: thesis: verum