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 ) )
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 )
thus for r, s, t being Element of S holds (r * s) * t = r * (s * t) by A1; :: according to GROUP_1:def 4 :: thesis: S is Group-like
consider r being Element of S;
consider s1 being Element of S such that
A3: r * s1 = r by A2;
consider s2 being Element of S such that
A4: s2 * r = r by A2;
consider t1 being Element of S such that
A5: r * t1 = s1 by A2;
A6: ex t2 being Element of S st t2 * r = s2 by A2;
A7: s1 = s2 * (r * t1) by A1, A4, A5
.= s2 by A1, A3, A5, A6 ;
take s1 ; :: according to GROUP_1:def 3 :: 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 * r = s by A2;
hence A8: s * s1 = s by A1, A3; :: thesis: ( s1 * s = s & ex g being Element of S st
( s * g = s1 & g * s = s1 ) )
ex t being Element of S st r * t = s by A2;
hence A9: s1 * s = s by A1, A4, A7; :: 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;
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;
take t1 ; :: thesis: ( s * t1 = s1 & t1 * s = s1 )
t1 = s1 * (s * r1) by A1, A9, A12
.= t2 * (s * t1) by A1, A11, A12
.= t2 by A1, A8, A10, A13 ;
hence ( s * t1 = s1 & t1 * s = s1 ) by A10, A11; :: thesis: verum