set W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);
A1:
for u, v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (u + v) + w = u + (v + w)
A2:
for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + (0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v
A3:
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable
proof
let v be
VECTOR of
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V #);
ALGSTR_0:def 16 v is right_complementable
reconsider v9 =
v as
VECTOR of
V ;
consider w9 being
VECTOR of
V such that A4:
v9 + w9 = 0. V
by ALGSTR_0:def 11;
reconsider w =
w9 as
VECTOR of
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V #) ;
take
w
;
ALGSTR_0:def 11 v + w = 0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
thus
v + w = 0. RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V #)
by A4;
verum
end;
A5:
for a being Real
for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds a * (v + w) = (a * v) + (a * w)
A6:
for a, b being Real
for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a * b) * v = a * (b * v)
A7:
for a, b being Real
for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a + b) * v = (a * v) + (b * v)
A8:
for a being Real
for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
for v9, w9 being VECTOR of V st v = v9 & w = w9 holds
( v + w = v9 + w9 & a * v = a * v9 )
;
A9:
for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + w = w + v
for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds 1 * v = v
then reconsider W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) as RealLinearSpace by A9, A1, A2, A3, A5, A7, A6, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;
A10:
the Mult of W = the Mult of V | [:REAL, 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
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V
by A10, Def2; verum