set K = { u where u is Element of V : T . u = 0. W } ;
{ u where u is Element of V : T . u = 0. W } c= [#] V

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { u where u is Element of V : T . u = 0. W } ; :: thesis:
then ex u being Element of V st
( u = x & T . u = 0. W ) ;
hence x in [#] V ; :: thesis:

end;

then reconsider K = { u where u is Element of V : T . u = 0. W } as Subset of V ;
A1: for v being Element of V st v in K holds
T . v = 0. W

let v be Element of V; :: thesis:
assume v in K ; :: thesis:
then ex u being Element of V st
( u = v & T . u = 0. W ) ;
hence T . v = 0. W ; :: thesis:

end;

let u be Element of V; :: thesis:
let a be Element of F; :: thesis:
assume u in K ; :: thesis:
then T . u = 0. W by A1;
then T . (a * u) = a * (0. W) by MOD_2:def 2
.= 0. W by VECTSP_1:14 ;
hence a * u in K ; :: thesis:

end;

then A2: for a being Element of F
for u being Element of V st u in K holds
a * u in K ;
T . (0. V) = 0. W by Th9;
then A3: 0. V in K ;

let u, v be Element of V; :: thesis:
assume ( u in K & v in K ) ; :: thesis:
then ( T . u = 0. W & T . v = 0. W ) by A1;
then T . (u + v) = (0. W) + (0. W) by VECTSP_1:def 20
.= 0. W by RLVECT_1:def 4 ;
hence u + v in K ; :: thesis:

end;

then K is linearly-closed by A2;
then consider W being strict Subspace of V such that
A4: K = the carrier of W by A3, VECTSP_4:34;
take W ; :: thesis:
thus [#] W = { u where u is Element of V : T . u = 0. W } by A4; :: thesis: