take S = Trivial-addLoopStr ; :: thesis: ( S is strict & S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable )
thus S is strict ; :: thesis: ( S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable )
thus S is Abelian :: thesis: ( S is add-associative & S is right_zeroed & S is right_complementable )

proof

let x be Element of S; :: according to RLVECT_1:def 5 :: thesis: for w being Element of S holds x + w = w + x
thus for w being Element of S holds x + w = w + x by STRUCT_0:def 10; :: thesis: verum

end;

thus S is add-associative :: thesis: ( S is right_zeroed & S is right_complementable )

proof

let x be Element of S; :: according to RLVECT_1:def 6 :: thesis: for v, w being Element of S holds (x + v) + w = x + (v + w)
thus for v, w being Element of S holds (x + v) + w = x + (v + w) by STRUCT_0:def 10; :: thesis: verum

end;

thus S is right_zeroed :: thesis: S is right_complementable

proof

let x be Element of S; :: according to RLVECT_1:def 7 :: thesis: x + (0. S) = x
thus x + (0. S) = x by STRUCT_0:def 10; :: thesis: verum

end;

thus S is right_complementable ; :: thesis: verum