let I be non empty closed_interval Subset of REAL; :: thesis: for D being Division of I
for T being Element of set_of_tagged_Division D holds rng T c= REAL
let D be Division of I; :: thesis: for T being Element of set_of_tagged_Division D holds rng T c= REAL
let T be Element of set_of_tagged_Division D; :: thesis: rng T c= REAL
ex s being non empty non-decreasing FinSequence of REAL st
( T = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) by Def2;
hence rng T c= REAL by FINSEQ_1:def 4; :: thesis: verum