let S be non empty multMagma ; :: 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 associative & S is Group-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 associative & S is Group-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 GROUP_1:def 3 :: thesis: S is Group-like
take s1 ; :: according to GROUP_1: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