theorem LMExtBit9: :: BINARI_6:21

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