theorem :: FOMODEL0:26

for Y being set
for f being Function st f is Y -valued & f is FinSequence-like holds
f is FinSequence of Y by Lm1;