let L be non empty addLoopStr ; :: thesis: for a being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) holds

(0. L) + a = a + (0. L)

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

assume that

A1: for a being Element of L holds a + (0. L) = a and

A2: for a being Element of L ex x being Element of L st a + x = 0. L and

A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) ; :: thesis: (0. L) + a = a + (0. L)

consider x being Element of L such that

A4: a + x = 0. L by A2;

thus (0. L) + a = a + (x + a) by A3, A4

.= a + (0. L) by A1, A2, A3, A4, Th1 ; :: thesis: verum

(0. L) + a = a + (0. L)

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

assume that

A1: for a being Element of L holds a + (0. L) = a and

A2: for a being Element of L ex x being Element of L st a + x = 0. L and

A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) ; :: thesis: (0. L) + a = a + (0. L)

consider x being Element of L such that

A4: a + x = 0. L by A2;

thus (0. L) + a = a + (x + a) by A3, A4

.= a + (0. L) by A1, A2, A3, A4, Th1 ; :: thesis: verum