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 ;
thus for a being Element of L holds (0. L) + a = a by A1, RLVECT_1:10; :: according to ALGSTR_1:def 5 :: thesis: L is Loop-like

now

thus for a, b being Element of L ex x being Element of L st a + x = b by A1, RLVECT_1:20; :: thesis: ( ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) )
thus for a, b being Element of L ex x being Element of L st x + a = b :: thesis: ( ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) )

proof

let a, b be Element of L; :: thesis: ex x being Element of L st x + a = b
reconsider a' = a, b' = b as Element of G ;
reconsider x = b' + (- a') as Element of L ;
take x ; :: thesis: x + a = b
(b' + (- a')) + a' = b' + ((- a') + a') by RLVECT_1:def 6
.= b' + (0. G) by RLVECT_1:16
.= b by RLVECT_1:10 ;
hence x + a = b ; :: thesis: verum

end;

thus ( ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) ) by A1, RLVECT_1:21; :: thesis: verum

end;

hence L is Loop-like by Th7; :: thesis: verum