consider A being finite Subset of W such that
A1: (Omega). W = Lin A by ZMODUL03:def 4;
( A c= the carrier of W & the carrier of W c= the carrier of V ) by VECTSP_4:def 2;
then reconsider A = A as finite Subset of V by XBOOLE_1:1;
reconsider Ws = (Omega). W as strict Subspace of V by ZMODUL01:42;
reconsider Lv = (Omega). (Lin {v}) as strict Subspace of V ;
Ws + Lv = (Lin A) + (Lin {v}) by A1, ZMODUL03:20
.= Lin (A \/ {v}) by ZMODUL02:72 ;
hence W + (Lin {v}) is finitely-generated by ZMODUL04:22; :: thesis: verum