Description: The vectors of a finite free module are the functions from I to N . (Contributed by SN, 31-Aug-2023)