theorem :: FINSEQ_6:109

for D being non empty set
for x being set
for f being FinSequence of D st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) )