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 )

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

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 )

end;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

thus
( ex v being Element of V st T . v = u implies u in U )
:: thesis: verum
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;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

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

u + v in U

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;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

now :: thesis: for a being Element of F

for w being Element of W st w in U holds

a * w in U

then A11:
U is linearly-closed
by A5;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;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

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