for A being finite set
for B being non empty set
for f being b₁ -defined b₂ -valued total Function holds f * (canFS A) is FinSequence of B