RL5Lm2:
for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat st n <= rank V holds
ex W being strict free Submodule of V st rank W = n
Th7:
for V, W being non empty 1-sorted
for T being Function of V,W holds
( dom T = [#] V & rng T c= [#] W )
by RANKNULL:7;
Lm1:
for V being Z_Module
for l being Z_Linear_Combination of V
for X being Subset of V holds l .: X is finite
ThTF3C1:
for V, W being non empty set
for A being finite Subset of V
for l being Function of V,W holds
( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )