theorem Th2: :: MEASURE9:4

for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for k being Nat st k < len F holds
Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*>