defpred S_{1}[ 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_{1}[n,y]

A2: for n being Element of NAT holds S_{1}[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

( 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

proof

consider f being sequence of ExtREAL such that
let n be Element of NAT ; :: thesis: ex y being Element of ExtREAL st S_{1}[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_{1}[n,y]

thus S_{1}[n,y]
; :: thesis: verum

end;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

thus S

A2: for n being Element of NAT holds S

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