let S be non empty addMagma ; ( ( for r, s, t being Element of S holds (r + s) + t = r + (s + t) ) & ( for r, s being Element of S holds
( ex t being Element of S st r + t = s & ex t being Element of S st t + r = s ) ) implies ( S is add-associative & S is addGroup-like ) )
set r = the Element of S;
assume that
A1:
for r, s, t being Element of S holds (r + s) + t = r + (s + t)
and
A2:
for r, s being Element of S holds
( ex t being Element of S st r + t = s & ex t being Element of S st t + r = s )
; ( S is add-associative & S is addGroup-like )
consider s1 being Element of S such that
A3:
the Element of S + s1 = the Element of S
by A2;
thus
for r, s, t being Element of S holds (r + s) + t = r + (s + t)
by A1; RLVECT_1:def 3 S is addGroup-like
take
s1
; GROUP_1A:def 2 for h being Element of S holds
( h + s1 = h & s1 + h = h & ex g being Element of S st
( h + g = s1 & g + h = s1 ) )
let s be Element of S; ( s + s1 = s & s1 + s = s & ex g being Element of S st
( s + g = s1 & g + s = s1 ) )
ex t being Element of S st t + the Element of S = s
by A2;
hence A4:
s + s1 = s
by A1, A3; ( s1 + s = s & ex g being Element of S st
( s + g = s1 & g + s = s1 ) )
consider s2 being Element of S such that
A5:
s2 + the Element of S = the Element of S
by A2;
consider t1 being Element of S such that
A6:
the Element of S + t1 = s1
by A2;
A7:
ex t2 being Element of S st t2 + the Element of S = s2
by A2;
A8: s1 =
s2 + ( the Element of S + t1)
by A1, A5, A6
.=
s2
by A1, A3, A6, A7
;
ex t being Element of S st the Element of S + t = s
by A2;
hence A9:
s1 + s = s
by A1, A5, A8; ex g being Element of S st
( s + g = s1 & g + s = s1 )
consider t1 being Element of S such that
A10:
s + t1 = s1
by A2;
consider t2 being Element of S such that
A11:
t2 + s = s1
by A2;
take
t1
; ( s + t1 = s1 & t1 + s = s1 )
consider r1 being Element of S such that
A12:
s + r1 = t1
by A2;
A13:
ex r2 being Element of S st r2 + s = t2
by A2;
t1 =
s1 + (s + r1)
by A1, A9, A12
.=
t2 + (s + t1)
by A1, A11, A12
.=
t2
by A1, A4, A10, A13
;
hence
( s + t1 = s1 & t1 + s = s1 )
by A10, A11; verum