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