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 )

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

assume u in U ; :: thesis:
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:
thus T . x = u by A3; :: thesis:

end;

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

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

end;

let u, v be Element of W; :: thesis:
assume that
A6: u in U and
A7: v in U ; :: thesis:
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:

end;

let a be Element of F; :: thesis:
let w be Element of W; :: thesis:
assume w in U ; :: thesis:
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:

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:
thus [#] A = T .: ([#] V) by A12; :: thesis: