let L be non empty addLoopStr ; :: thesis: ( L is add-associative & L is right_zeroed & L is right_complementable implies ( L is left_zeroed & L is Loop-like ) )

assume A1: ( L is add-associative & L is right_zeroed & L is right_complementable ) ; :: thesis: ( L is left_zeroed & L is Loop-like )

then reconsider G = L as non empty right_complementable add-associative right_zeroed addLoopStr ;

A2: for a, x, y being Element of L st x + a = y + a holds

x = y by A1, RLVECT_1:8;

thus for a being Element of L holds (0. L) + a = a by A1, RLVECT_1:4; :: according to ALGSTR_1:def 2 :: thesis: L is Loop-like

A3: for a, b being Element of L ex x being Element of L st x + a = b

x = y ) ) by A1, RLVECT_1:7, RLVECT_1:8;

hence L is Loop-like by A3, A2, Th6; :: thesis: verum

assume A1: ( L is add-associative & L is right_zeroed & L is right_complementable ) ; :: thesis: ( L is left_zeroed & L is Loop-like )

then reconsider G = L as non empty right_complementable add-associative right_zeroed addLoopStr ;

A2: for a, x, y being Element of L st x + a = y + a holds

x = y by A1, RLVECT_1:8;

thus for a being Element of L holds (0. L) + a = a by A1, RLVECT_1:4; :: according to ALGSTR_1:def 2 :: thesis: L is Loop-like

A3: for a, b being Element of L ex x being Element of L st x + a = b

proof

( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( for a, x, y being Element of L st a + x = a + y holds
let a, b be Element of L; :: thesis: ex x being Element of L st x + a = b

reconsider a9 = a, b9 = b as Element of G ;

reconsider x = b9 + (- a9) as Element of L ;

take x ; :: thesis: x + a = b

(b9 + (- a9)) + a9 = b9 + ((- a9) + a9) by RLVECT_1:def 3

.= b9 + (0. G) by RLVECT_1:5

.= b by RLVECT_1:4 ;

hence x + a = b ; :: thesis: verum

end;reconsider a9 = a, b9 = b as Element of G ;

reconsider x = b9 + (- a9) as Element of L ;

take x ; :: thesis: x + a = b

(b9 + (- a9)) + a9 = b9 + ((- a9) + a9) by RLVECT_1:def 3

.= b9 + (0. G) by RLVECT_1:5

.= b by RLVECT_1:4 ;

hence x + a = b ; :: thesis: verum

x = y ) ) by A1, RLVECT_1:7, RLVECT_1:8;

hence L is Loop-like by A3, A2, Th6; :: thesis: verum