theorem Th26: :: PRE_POLY:27

for D being set
for F being FinSequence of D * holds len (FlattenSeq F) = Sum (Card F)