consider a, b being Real such that
A1: I = [.a,b.] by MEASURE5:def 3;
A2: a <= b by A1, XXREAL_1:29;
reconsider B = <*b*> as Division of I by A1, Th35;
now :: thesis: ( dom <*b*> = dom B & ( for i being Nat st i in dom B holds
<*b*> . i in divset (B,i) ) )
thus dom <*b*> = dom B ; :: thesis: for i being Nat st i in dom B holds
<*b*> . i in divset (B,i)
hereby :: thesis: verum
let i be Nat; :: thesis: ( i in dom B implies <*b*> . i in divset (B,i) )
assume A3: i in dom B ; :: thesis: <*b*> . i in divset (B,i)
then A4: i in {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then A5: i = 1 by TARSKI:def 1;
consider c, d being Real such that
A6: divset (B,1) = [.c,d.] by MEASURE5:def 3;
A7: c <= d by A6, XXREAL_1:29;
1 in dom B by A3, A4, TARSKI:def 1;
then ( lower_bound (divset (B,1)) = lower_bound [.a,b.] & upper_bound (divset (B,1)) = B . 1 ) by A1, INTEGRA1:def 4;
then ( c = lower_bound [.a,b.] & d = B . 1 ) by A7, A6, JORDAN5A:19;
then A8: ( c = a & d = b ) by FINSEQ_1:def 8, A2, JORDAN5A:19;
b in [.a,b.] by A2, XXREAL_1:1;
hence <*b*> . i in divset (B,i) by A8, A6, A5, FINSEQ_1:def 8; :: thesis: verum
end;
end;
then reconsider T = <*b*> as Element of set_of_tagged_Division B by Def2;
take [B,T] ; :: thesis: ex D being Division of I ex T being Element of set_of_tagged_Division D st [B,T] = [D,T]
thus ex D being Division of I ex T being Element of set_of_tagged_Division D st [B,T] = [D,T] ; :: thesis: verum