theorem Th5: :: ARMSTRNG:5

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