theorem Th1: :: LTLAXIO3:1

for X being non empty set
for t being FinSequence of X
for k being Nat st k + 1 <= len t holds
t /^ k = <*(t . (k + 1))*> ^ (t /^ (k + 1))