theorem Th3: :: FRIENDS1:3

for k, n being Nat
for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) & k <= n & n <= len p holds
p = (q /^ (n -' k)) ^ (q | (n -' k))