reconsider W = (0). V as strict free Submodule of V ;
take W ; :: thesis: ( W is strict & W is finite-rank )
thus ( W is strict & W is finite-rank ) ; :: thesis: verum