theorem Th3: :: MATRIX14:3

for L being non empty addLoopStr
for x1, x2 being FinSequence of L st len x1 = len x2 holds
len (x1 - x2) = len x1