let S be 1 -element addLoopStr ; :: thesis: ( S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable )

thus ( ( for v, w being Element of S holds v + w = w + v ) & ( for u, v, w being Element of S holds (u + v) + w = u + (v + w) ) & ( for v being Element of S holds v + (0. S) = v ) ) by STRUCT_0:def 10; :: according to RLVECT_1:def 2,RLVECT_1:def 3,RLVECT_1:def 4 :: thesis: S is right_complementable

let v be Element of S; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

take v ; :: according to ALGSTR_0:def 11 :: thesis: v + v = 0. S

thus v + v = 0. S by STRUCT_0:def 10; :: thesis: verum

thus ( ( for v, w being Element of S holds v + w = w + v ) & ( for u, v, w being Element of S holds (u + v) + w = u + (v + w) ) & ( for v being Element of S holds v + (0. S) = v ) ) by STRUCT_0:def 10; :: according to RLVECT_1:def 2,RLVECT_1:def 3,RLVECT_1:def 4 :: thesis: S is right_complementable

let v be Element of S; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

take v ; :: according to ALGSTR_0:def 11 :: thesis: v + v = 0. S

thus v + v = 0. S by STRUCT_0:def 10; :: thesis: verum