let I be non empty closed_interval Subset of REAL; :: thesis: for TD being tagged_division of I holds len (tagged_of TD) = len (division_of TD)
let TD be tagged_division of I; :: thesis: len (tagged_of TD) = len (division_of TD)
consider D being Division of I, T being Element of set_of_tagged_Division D such that
A1: TD = [D,T] by COUSIN:def 3;
consider s being non empty non-decreasing FinSequence of REAL such that
A2: T = s and
A3: dom s = dom D and
for i being Nat st i in dom s holds
s . i in divset (D,i) by COUSIN:def 2;
( tagged_of TD = T & division_of TD = D ) by A1, Th20;
hence len (tagged_of TD) = len (division_of TD) by A2, A3, FINSEQ_3:29; :: thesis: verum