theorem :: FILEREC1:12

for a, b being set
for D being non empty set
for f being FinSequence of D st f = <*a,b*> holds
f /^ 1 = <*b*>