theorem LMExtBit7: :: BINARI_6:24

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN
for x1, y1 being Tuple of K + 1, BOOLEAN st not x,y are_summable & x1 = x ^ <*0*> & y1 = y ^ <*0*> holds
(x1 + y1) . (len (x1 + y1)) = 1