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 Def3, Def4, ALGSTR_0:def 3, ALGSTR_0:def 4; :: 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 that

A1: ( ( 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 ) ) and

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

x = y and

A3: 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 5 :: thesis: ( L is right_add-cancelable & L is add-left-invertible & L is add-right-invertible )

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 Def3, Def4, ALGSTR_0:def 3, ALGSTR_0:def 4; :: 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 that

A1: ( ( 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 ) ) and

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

x = y and

A3: 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 5 :: thesis: ( L is right_add-cancelable & L is add-left-invertible & L is add-right-invertible )

proof

thus
L is right_add-cancelable
:: thesis: ( L is add-left-invertible & L is add-right-invertible )
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 ( not x + x = x + x or x = x ) by A2; :: thesis: verum

proof

thus
( L is add-left-invertible & L is add-right-invertible )
by A1; :: thesis: verum
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 A3; :: thesis: verum

end;thus ( not x + x = x + x or x = x ) by A3; :: thesis: verum