theorem :: FILEREC1:15

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 = <*b,c*>