theorem Th5: :: FRIENDS1:5

for k, n being Nat
for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) holds
ex i being Nat st p = (q /^ i) ^ (q | i)