let L be non empty addLoopStr ; :: thesis: ( L is Abelian & L is right_complementable implies L is left_complementable )
assume A2: ( L is Abelian & L is right_complementable ) ; :: thesis: L is left_complementable
let a be Element of L; :: according to ALGSTR_0:def 15 :: thesis: a is left_complementable
consider w being Element of L such that
A3: a + w = 0. L by A2, ALGSTR_0:def 11;
take w ; :: according to ALGSTR_0:def 10 :: thesis: w + a = 0. L
thus w + a = 0. L by A2, A3; :: thesis: verum