theorem Th8: :: IDEA_1:8

for n being Nat
for x being Tuple of n, BOOLEAN holds (ZERO n) 'xor' x = x