theorem Th2: :: GR_FREE0:2

for p being FinSequence st len p <> 0 holds
p /^ ((len p) -' 1) = <*(p . (len p))*>