theorem Th1: :: UNIROOTS:1

for f being FinSequence st 1 <= len f holds
f | (Seg 1) = <*(f . 1)*>