theorem Th14: :: FINSEQ_5:14
for f being FinSequence st len f = 1 holds
f = <*(f . 1)*> by FINSEQ_1:40;