set M = the lmult of V;

set W = ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #);

A1: ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is vector-distributive

for x, y being Element of V st x = a & b = y holds

a + b = x + y ;

( ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Abelian & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is add-associative & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable )

A6: ( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19;

the lmult of W = the lmult of V | [: the carrier of GF, the carrier of W:] by RELSET_1:19;

then reconsider W = W as Subspace of V by A6, Def2;

take W ; :: thesis: W is strict

thus W is strict ; :: thesis: verum

set W = ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #);

A1: ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is vector-distributive

proof

A2:
ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-distributive
let a be Element of GF; :: according to VECTSP_1:def 13 :: thesis: for b_{1}, b_{2} being Element of the carrier of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) holds a * (b_{1} + b_{2}) = (a * b_{1}) + (a * b_{2})

let v, w be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider x = v, y = w as Element of V ;

thus a * (v + w) = a * (x + y)

.= (a * x) + (a * y) by VECTSP_1:def 14

.= (a * v) + (a * w) ; :: thesis: verum

end;let v, w be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider x = v, y = w as Element of V ;

thus a * (v + w) = a * (x + y)

.= (a * x) + (a * y) by VECTSP_1:def 14

.= (a * v) + (a * w) ; :: thesis: verum

proof

A3:
ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-associative
let a, b be Element of GF; :: according to VECTSP_1:def 14 :: thesis: for b_{1} being Element of the carrier of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) holds (a + b) * b_{1} = (a * b_{1}) + (b * b_{1})

let v be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider x = v as Element of V ;

thus (a + b) * v = (a + b) * x

.= (a * x) + (b * x) by VECTSP_1:def 15

.= (a * v) + (b * v) ; :: thesis: verum

end;let v be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider x = v as Element of V ;

thus (a + b) * v = (a + b) * x

.= (a * x) + (b * x) by VECTSP_1:def 15

.= (a * v) + (b * v) ; :: thesis: verum

proof

A4:
ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-unital
let a, b be Element of GF; :: according to VECTSP_1:def 15 :: thesis: for b_{1} being Element of the carrier of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) holds (a * b) * b_{1} = a * (b * b_{1})

let v be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: (a * b) * v = a * (b * v)

reconsider x = v as Element of V ;

thus (a * b) * v = (a * b) * x

.= a * (b * x) by VECTSP_1:def 16

.= a * (b * v) ; :: thesis: verum

end;let v be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: (a * b) * v = a * (b * v)

reconsider x = v as Element of V ;

thus (a * b) * v = (a * b) * x

.= a * (b * x) by VECTSP_1:def 16

.= a * (b * v) ; :: thesis: verum

proof

A5:
for a, b being Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
let v be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: according to VECTSP_1:def 16 :: thesis: (1. GF) * v = v

reconsider x = v as Element of V ;

thus (1. GF) * v = (1_ GF) * x

.= v by VECTSP_1:def 17 ; :: thesis: verum

end;reconsider x = v as Element of V ;

thus (1. GF) * v = (1_ GF) * x

.= v by VECTSP_1:def 17 ; :: thesis: verum

for x, y being Element of V st x = a & b = y holds

a + b = x + y ;

( ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Abelian & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is add-associative & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable )

proof

then reconsider W = ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF by A1, A2, A3, A4;
thus
ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Abelian
:: thesis: ( ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is add-associative & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable )

reconsider x = a as Element of V ;

reconsider b = (comp V) . x as Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) ;

take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)

thus a + b = x + (- x) by VECTSP_1:def 13

.= 0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) by RLVECT_1:5 ; :: thesis: verum

end;proof

let a, b be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a

reconsider x = a, y = b as Element of V ;

thus a + b = y + x by A5

.= b + a ; :: thesis: verum

end;reconsider x = a, y = b as Element of V ;

thus a + b = y + x by A5

.= b + a ; :: thesis: verum

hereby :: according to RLVECT_1:def 3 :: thesis: ( ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable )

let a, b, c be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: (a + b) + c = a + (b + c)

reconsider x = a, y = b, z = c as Element of V ;

thus (a + b) + c = (x + y) + z

.= x + (y + z) by RLVECT_1:def 3

.= a + (b + c) ; :: thesis: verum

end;reconsider x = a, y = b, z = c as Element of V ;

thus (a + b) + c = (x + y) + z

.= x + (y + z) by RLVECT_1:def 3

.= a + (b + c) ; :: thesis: verum

hereby :: according to RLVECT_1:def 4 :: thesis: ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable

let a be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable let a be Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #); :: thesis: a + (0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)) = a

reconsider x = a as Element of V ;

thus a + (0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)) = x + (0. V)

.= a by RLVECT_1:4 ; :: thesis: verum

end;reconsider x = a as Element of V ;

thus a + (0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)) = x + (0. V)

.= a by RLVECT_1:4 ; :: thesis: verum

reconsider x = a as Element of V ;

reconsider b = (comp V) . x as Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) ;

take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)

thus a + b = x + (- x) by VECTSP_1:def 13

.= 0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) by RLVECT_1:5 ; :: thesis: verum

A6: ( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19;

the lmult of W = the lmult of V | [: the carrier of GF, the carrier of W:] by RELSET_1:19;

then reconsider W = W as Subspace of V by A6, Def2;

take W ; :: thesis: W is strict

thus W is strict ; :: thesis: verum