theorem LMExtBit2: :: BINARI_6:15

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