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

proof

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;

( ( 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
x = y ) ) by A1, RLVECT_1:7, RLVECT_1:8;
hence L is Loop-like by A3, A2, Th6; :: thesis: verum