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
A2:
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is scalar-distributive
A3:
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is scalar-associative
A4:
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is scalar-unital
A5:
for a being Element of GF
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
thus
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 )
let x be
Element of
ModuleStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
lmult of
V #);
ALGSTR_0:def 16 x 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
;
ALGSTR_0:def 11 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;
verum
end;
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;
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; verum