theorem Th53: :: AFINSQ_1:56

for n being Nat
for p being XFinSequence st len p = n + 1 holds
p = (p | n) ^ <%(p . n)%>