theorem :: FILEREC1:11

for a being set
for f being FinSequence st f = <*a*> holds
f | 1 = <*a*>