:: deftheorem Def1 defines Length MEASURE9:def 1 :
for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for b₄ being FinSequence of NAT holds
( b₄ = Length F iff ( dom b₄ = dom F & ( for n being Nat st n in dom b₄ holds
b₄ . n = len (F . n) ) ) );