let S be non empty addMagma ; :: thesis: ( ( 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 ) ; :: thesis: ( 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; :: according to RLVECT_1:def 3 :: thesis: S is addGroup-like
take s1 ; :: according to GROUP_1A:def 2 :: thesis: 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum