theorem Th20: :: FINSEQ_5:20

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