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= I
let D be Division of I; :: thesis: for T being Element of set_of_tagged_Division D holds rng T c= I
let T be Element of set_of_tagged_Division D; :: thesis: rng T c= I
consider s being non empty non-decreasing FinSequence of REAL such that
A1: ( T = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) by COUSIN:def 2;
now :: thesis: for x being object st x in rng T holds
x in I
let x be object ; :: thesis: ( x in rng T implies x in I )
assume x in rng T ; :: thesis: x in I
then consider y being object such that
A2: y in dom T and
A3: x = T . y by FUNCT_1:def 3;
reconsider y = y as Nat by A2;
divset (D,y) c= I by A1, A2, INTEGRA1:8;
hence x in I by A3, A1, A2; :: thesis: verum
end;
hence rng T c= I ; :: thesis: verum