for V, W being non empty set
for f being FinSequence
for l being Function of V,W st rng f c= V holds
( l * f is W -valued & l * f is FinSequence-like )