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