theorem Th20: :: FINSEQ_5:20

for D being set
for f being FinSequence of D st not f is empty holds
f | 1 = <*(f /. 1)*>