theorem :: ARMSTRNG:6

for n being Element of NAT
for p being Tuple of n, BOOLEAN holds ('not' (n -BinarySequence 0)) '&' p = p