theorem Th14: :: FINSEQ_5:14

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