theorem Th4: :: FRIENDS1:4

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