theorem Th1: :: NBVECTSP:1

for n being non zero Element of NAT
for u1, v1, w1 being Element of n -tuples_on BOOLEAN holds Op-XOR ((Op-XOR (u1,v1)),w1) = Op-XOR (u1,(Op-XOR (v1,w1)))