reconsider U = T .: ([#] V) as Subset of W ;
A1: for u being Element of W holds
( u in U iff ex v being Element of V st T . v = u )

proof

let u be Element of W; :: thesis: ( u in U iff ex v being Element of V st T . v = u )
thus ( u in U implies ex v being Element of V st T . v = u ) :: thesis: ( ex v being Element of V st T . v = u implies u in U )

proof

assume u in U ; :: thesis: ex v being Element of V st T . v = u
then consider x being object such that
x in dom T and
A2: x in [#] V and
A3: u = T . x by FUNCT_1:def 6;
reconsider x = x as Element of V by A2;
take x ; :: thesis: T . x = u
thus T . x = u by A3; :: thesis: verum

end;

thus ( ex v being Element of V st T . v = u implies u in U ) :: thesis: verum

proof

given v being Element of V such that A4: T . v = u ; :: thesis: u in U
v in [#] V ;
then v in dom T by Th7;
hence u in U by A4, FUNCT_1:def 6; :: thesis: verum

end;

end;

A5: now :: thesis: for u, v being Element of W st u in U & v in U holds
u + v in U

let u, v be Element of W; :: thesis: ( u in U & v in U implies u + v in U )
assume that
A6: u in U and
A7: v in U ; :: thesis: u + v in U
consider x being Element of V such that
A8: T . x = u by A1, A6;
consider y being Element of V such that
A9: T . y = v by A1, A7;
u + v = T . (x + y) by A8, A9, VECTSP_1:def 20;
hence u + v in U by A1; :: thesis: verum

end;

now :: thesis: for a being Element of F
for w being Element of W st w in U holds
a * w in U

let a be Element of F; :: thesis: for w being Element of W st w in U holds
a * w in U
let w be Element of W; :: thesis: ( w in U implies a * w in U )
assume w in U ; :: thesis: a * w in U
then consider v being Element of V such that
A10: T . v = w by A1;
T . (a * v) = a * w by A10, MOD_2:def 2;
hence a * w in U by A1; :: thesis: verum

end;

then A11: U is linearly-closed by A5;
T . (0. V) = 0. W by Th9;
then U <> {} by A1;
then consider A being strict Subspace of W such that
A12: U = the carrier of A by A11, VECTSP_4:34;
take A ; :: thesis: [#] A = T .: ([#] V)
thus [#] A = T .: ([#] V) by A12; :: thesis: verum