theorem :: BINARI_4:19

for n being non zero Nat
for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
x,y are_summable