for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y st ( for n being Nat st n in dom F holds
F . n = <*> D ) holds
Sum (Length F) = 0