let L be non empty addLoopStr ; :: thesis: ( L is Loop-like iff ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( 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 ( L is Loop-like implies ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( 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 ) ) ) by Lm7, Lm8, Def8, Def9; :: thesis: ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( 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 ) implies L is Loop-like )
assume A2: ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( 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 ) ) ; :: thesis: L is Loop-like
thus L is left_add-cancelable :: according to ALGSTR_1:def 12 :: thesis: ( L is right_add-cancelable & L is add-left-invertible & L is add-right-invertible )

proof

let x, x, x be Element of L; :: according to ALGSTR_0:def 3,ALGSTR_0:def 6 :: thesis: ( not x + x = x + x or x = x )
thus ( not x + x = x + x or x = x ) by A2; :: thesis: verum

end;

thus L is right_add-cancelable :: thesis: ( L is add-left-invertible & L is add-right-invertible )

proof

let x, x, x be Element of L; :: according to ALGSTR_0:def 4,ALGSTR_0:def 7 :: thesis: ( not x + x = x + x or x = x )
thus ( not x + x = x + x or x = x ) by A2; :: thesis: verum

end;

thus ( L is add-left-invertible & L is add-right-invertible ) by A2, Def8, Def9; :: thesis: verum