let seq be ExtREAL_sequence; :: thesis: for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL
let n be Element of NAT ; :: thesis: { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL
deffunc H₁( Element of NAT ) -> Element of ExtREAL = seq . $1;
defpred S₁[ Element of NAT ] means n <= $1;
set Y = { H₁(k) where k is Element of NAT : S₁[k] } ;
A1: seq . n in { H₁(k) where k is Element of NAT : S₁[k] } ;
{ H₁(k) where k is Element of NAT : S₁[k] } is Subset of ExtREAL from DOMAIN_1:sch 8();
hence { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL by A1; :: thesis: verum