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

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

for v, w being Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

for v9, w9 being Element of V st v = v9 & w = w9 holds

( v + w = v9 + w9 & a * v = a * v9 ) ;

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

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

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

hence ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V by A7, Def2; :: thesis: verum

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

proof

A2:
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is scalar-distributive
let x 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, the ZeroF of V, the lmult of V #) holds x * (b_{1} + b_{2}) = (x * b_{1}) + (x * b_{2})

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

reconsider v9 = v, w9 = w as Element of V ;

thus x * (v + w) = x * (v9 + w9)

.= (x * v9) + (x * w9) by VECTSP_1:def 14

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

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

reconsider v9 = v, w9 = w as Element of V ;

thus x * (v + w) = x * (v9 + w9)

.= (x * v9) + (x * w9) by VECTSP_1:def 14

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

proof

A3:
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is scalar-associative
let x, y 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, the ZeroF of V, the lmult of V #) holds (x + y) * b_{1} = (x * b_{1}) + (y * b_{1})

let v be Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); :: thesis: (x + y) * v = (x * v) + (y * v)

reconsider v9 = v as Element of V ;

thus (x + y) * v = (x + y) * v9

.= (x * v9) + (y * v9) by VECTSP_1:def 15

.= (x * v) + (y * v) ; :: thesis: verum

end;let v be Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); :: thesis: (x + y) * v = (x * v) + (y * v)

reconsider v9 = v as Element of V ;

thus (x + y) * v = (x + y) * v9

.= (x * v9) + (y * v9) by VECTSP_1:def 15

.= (x * v) + (y * v) ; :: thesis: verum

proof

A4:
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is scalar-unital
let x, y 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, the ZeroF of V, the lmult of V #) holds (x * y) * b_{1} = x * (y * b_{1})

let v be Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); :: thesis: (x * y) * v = x * (y * v)

reconsider v9 = v as Element of V ;

thus (x * y) * v = (x * y) * v9

.= x * (y * v9) by VECTSP_1:def 16

.= x * (y * v) ; :: thesis: verum

end;let v be Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); :: thesis: (x * y) * v = x * (y * v)

reconsider v9 = v as Element of V ;

thus (x * y) * v = (x * y) * v9

.= x * (y * v9) by VECTSP_1:def 16

.= x * (y * v) ; :: thesis: verum

proof

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

reconsider v9 = v as Element of V ;

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

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

end;reconsider v9 = v as Element of V ;

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

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

for v, w being Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

for v9, w9 being Element of V st v = v9 & w = w9 holds

( v + w = v9 + w9 & a * v = a * v9 ) ;

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

proof

then reconsider W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of 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 A4, A1, A2, A3;
thus
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is Abelian
:: thesis: ( ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is add-associative & ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is right_complementable )

reconsider x9 = x as Element of V ;

consider b being Element of V such that

A6: x9 + b = 0. V by ALGSTR_0:def 11;

reconsider b9 = b as Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ;

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

thus x + b9 = 0. ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A6; :: thesis: verum

end;proof

let x, y be Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x

reconsider x9 = x, y9 = y as Element of V ;

thus x + y = y9 + x9 by A5

.= y + x ; :: thesis: verum

end;reconsider x9 = x, y9 = y as Element of V ;

thus x + y = y9 + x9 by A5

.= y + x ; :: thesis: verum

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

let x, y, z be Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #); :: thesis: (x + y) + z = x + (y + z)

reconsider x9 = x, y9 = y, z9 = z as Element of V ;

thus (x + y) + z = (x9 + y9) + z9

.= x9 + (y9 + z9) by RLVECT_1:def 3

.= x + (y + z) ; :: thesis: verum

end;reconsider x9 = x, y9 = y, z9 = z as Element of V ;

thus (x + y) + z = (x9 + y9) + z9

.= x9 + (y9 + z9) by RLVECT_1:def 3

.= x + (y + z) ; :: thesis: verum

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

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

reconsider x9 = x as Element of V ;

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

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

end;reconsider x9 = x as Element of V ;

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

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

reconsider x9 = x as Element of V ;

consider b being Element of V such that

A6: x9 + b = 0. V by ALGSTR_0:def 11;

reconsider b9 = b as Element of ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ;

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

thus x + b9 = 0. ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A6; :: thesis: verum

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

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

hence ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V by A7, Def2; :: thesis: verum