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

proof

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

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

proof

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

end;

now :: thesis: for u being Element of V
for a being Element of F st u in K holds
a * u in K

let u be Element of V; :: thesis: for a being Element of F st u in K holds
a * u in K
let a be Element of F; :: thesis: ( u in K implies a * u in K )
assume u in K ; :: thesis: a * u in K
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: verum

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 ;

now :: thesis: for u, v being Element of V st u in K & v in K holds
u + v in K

let u, v be Element of V; :: thesis: ( u in K & v in K implies u + v in K )
assume ( u in K & v in K ) ; :: thesis: u + v in K
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: verum

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: [#] W = { u where u is Element of V : T . u = 0. W }
thus [#] W = { u where u is Element of V : T . u = 0. W } by A4; :: thesis: verum