let n be Nat; :: thesis: for seq being ExtREAL_sequence holds

( inf seq <= seq . n & seq . n <= sup seq )

let seq be ExtREAL_sequence; :: thesis: ( inf seq <= seq . n & seq . n <= sup seq )

A1: inf (rng seq) is LowerBound of rng seq by XXREAL_2:def 4;

A2: sup (rng seq) is UpperBound of rng seq by XXREAL_2:def 3;

n in NAT by ORDINAL1:def 12;

then seq . n in rng seq by FUNCT_2:4;

hence ( inf seq <= seq . n & seq . n <= sup seq ) by A1, A2, XXREAL_2:def 1, XXREAL_2:def 2; :: thesis: verum

( inf seq <= seq . n & seq . n <= sup seq )

let seq be ExtREAL_sequence; :: thesis: ( inf seq <= seq . n & seq . n <= sup seq )

A1: inf (rng seq) is LowerBound of rng seq by XXREAL_2:def 4;

A2: sup (rng seq) is UpperBound of rng seq by XXREAL_2:def 3;

n in NAT by ORDINAL1:def 12;

then seq . n in rng seq by FUNCT_2:4;

hence ( inf seq <= seq . n & seq . n <= sup seq ) by A1, A2, XXREAL_2:def 1, XXREAL_2:def 2; :: thesis: verum