theorem :: FILEREC1:13

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 | 1 = <*a*>