theorem Th13: :: AFINSQ_2:13

for n being Nat
for p being XFinSequence holds (p | n) ^ (p /^ n) = p