:: deftheorem Def3 defines Length MEASURE9:def 3 :
for D being set
for Y being FinSequenceSet of D
for s being sequence of Y
for b₄ being sequence of NAT holds
( b₄ = Length s iff for n being Nat holds b₄ . n = len (s . n) );