theorem Th1: :: MATRIX14:1

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