for D being non empty set
for p being FinSequence of D
for n being Element of NAT st 1 <= n & n <= len p holds
p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) by FINSEQ_5:84;