take S = Trivial-RLSStruct ; :: thesis: ( S is strict & S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
thus S is strict ; :: thesis: ( S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
thus S is Abelian by STRUCT_0:def 10; :: thesis: ( S is add-associative & S is right_zeroed & S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
thus S is add-associative by STRUCT_0:def 10; :: thesis: ( S is right_zeroed & S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
thus S is right_zeroed by STRUCT_0:def 10; :: thesis: ( S is right_complementable & S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )
thus S is right_complementable :: thesis: ( S is scalar-distributive & S is vector-distributive & S is scalar-associative & S is scalar-unital )

proof

let x be Element of S; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
take x ; :: according to ALGSTR_0:def 11 :: thesis: x + x = 0. S
thus x + x = 0. S by STRUCT_0:def 10; :: thesis: verum

end;

thus for a, b being Real
for v being VECTOR of S holds (a + b) * v = (a * v) + (b * v) by STRUCT_0:def 10; :: according to RLVECT_1:def 6 :: thesis: ( S is vector-distributive & S is scalar-associative & S is scalar-unital )
thus for a being Real
for v, w being VECTOR of S holds a * (v + w) = (a * v) + (a * w) by STRUCT_0:def 10; :: according to RLVECT_1:def 5 :: thesis: ( S is scalar-associative & S is scalar-unital )
thus for a, b being Real
for v being VECTOR of S holds (a * b) * v = a * (b * v) by STRUCT_0:def 10; :: according to RLVECT_1:def 7 :: thesis: S is scalar-unital
thus for v being VECTOR of S holds 1 * v = v by STRUCT_0:def 10; :: according to RLVECT_1:def 8 :: thesis: verum