let L be non empty addLoopStr ; 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; ( ( 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)
; (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
; verum