for L being non empty addLoopStr
for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F