theorem Th1: :: GR_FREE0:1

for p being FinSequence st len p <> 0 holds
p | 1 = <*(p . 1)*>