theorem Th14: :: FILEREC1:14

for a, b, c being set
for D being non empty set
for f being FinSequence of D st f = <*a,b,c*> holds
f | 2 = <*a,b*>