theorem LMExtBit61: :: BINARI_6:22

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x,y are_summable holds
y,x are_summable