let L be non empty addLoopStr ; :: thesis: ( L is AddGroup iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) ) )

thus ( L is AddGroup implies ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) ) ) by Th6, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) implies L is AddGroup )

assume that

A1: for a being Element of L holds a + (0. L) = a and

A2: for a being Element of L ex x being Element of L st a + x = 0. L and

A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) ; :: thesis: L is AddGroup

L is right_complementable

thus ( L is AddGroup implies ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) ) ) by Th6, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) implies L is AddGroup )

assume that

A1: for a being Element of L holds a + (0. L) = a and

A2: for a being Element of L ex x being Element of L st a + x = 0. L and

A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) ; :: thesis: L is AddGroup

L is right_complementable

proof

hence
L is AddGroup
by A1, A3, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum
let a be Element of L; :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable

thus ex x being Element of L st a + x = 0. L by A2; :: according to ALGSTR_0:def 11 :: thesis: verum

end;thus ex x being Element of L st a + x = 0. L by A2; :: according to ALGSTR_0:def 11 :: thesis: verum