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 set ; :: 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 A1: x in { u where u is Element of V : T . u = 0. W } ; :: thesis: x in [#] V
consider u being Element of V such that
A2: u = x and
T . u = 0. W by A1;
thus x in [#] V by A2; :: thesis: verum

end;

then reconsider K = { u where u is Element of V : T . u = 0. W } as Subset of V ;
A3: 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 A4: v in K ; :: thesis: T . v = 0. W
consider u being Element of V such that
A5: u = v and
A6: T . u = 0. W by A4;
thus T . v = 0. W by A5, A6; :: thesis: verum

end;

( K <> {} & K is linearly-closed )

proof

T . (0. V) = 0. W by Th9;
then 0. V in K ;
hence K <> {} ; :: thesis: K is linearly-closed
thus K is linearly-closed :: thesis: verum

proof

A7: now

let u, v be Element of V; :: thesis: ( u in K & v in K implies u + v in K )
assume that
A8: u in K and
A9: v in K ; :: thesis: u + v in K
A10: T . u = 0. W by A3, A8;
T . v = 0. W by A3, A9;
then T . (u + v) = (0. W) + (0. W) by A10, MOD_2:def 5
.= 0. W by RLVECT_1:def 7 ;
hence u + v in K ; :: thesis: verum

end;

now

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 A11: u in K ; :: thesis: a * u in K
T . u = 0. W by A3, A11;
then T . (a * u) = a * (0. W) by MOD_2:def 5
.= 0. W by VECTSP_1:59 ;
hence a * u in K ; :: thesis: verum

end;

then for a being Element of F
for u being Element of V st u in K holds
a * u in K ;
hence K is linearly-closed by A7, VECTSP_4:def 1; :: thesis: verum

end;

end;

then consider W being strict Subspace of V such that
A12: K = the carrier of W by VECTSP_4:42;
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 A12; :: thesis: verum