for L being non empty addLoopStr
for x being FinSequence of L holds x is Element of (len x) -tuples_on the carrier of L