theorem LMExtBit6: :: BINARI_6:23

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x,y are_summable & ( x . (len x) = 1 or y . (len y) = 1 ) holds
(x + y) . (len (x + y)) = 1