theorem :: AFINSQ_1:60

for n being Nat
for p being XFinSequence ex q being XFinSequence st p = (p | n) ^ q