the carrier of (SymGroup X) = permutations X by Def2;
hence not the carrier of (SymGroup X) is empty ; :: according to STRUCT_0:def 1 :: thesis: ( SymGroup X is associative & SymGroup X is Group-like )
thus SymGroup X is associative :: thesis: SymGroup X is Group-like
proof
let x, y, z be Element of (SymGroup X); :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
thus (x * y) * z = z * (x * y) by Def2
.= z * (y * x) by Def2
.= (z * y) * x by RELAT_1:36
.= (y * z) * x by Def2
.= x * (y * z) by Def2 ; :: thesis: verum
end;
set e = id X;
id X in permutations X ;
then reconsider e = id X as Element of (SymGroup X) by Def2;
take e ; :: according to GROUP_1:def 2 :: thesis: for b1 being Element of the carrier of (SymGroup X) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (SymGroup X) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of (SymGroup X); :: thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (SymGroup X) st
( h * b1 = e & b1 * h = e ) )
reconsider h1 = h as Permutation of X by Th5;
thus h * e = e * h1 by Def2
.= h by FUNCT_2:17 ; :: thesis: ( e * h = h & ex b1 being Element of the carrier of (SymGroup X) st
( h * b1 = e & b1 * h = e ) )
thus e * h = h1 * e by Def2
.= h by FUNCT_2:17 ; :: thesis: ex b1 being Element of the carrier of (SymGroup X) st
( h * b1 = e & b1 * h = e )
h1 " in permutations X ;
then reconsider g = h1 " as Element of (SymGroup X) by Def2;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = g * h by Def2
.= e by FUNCT_2:61 ; :: thesis: g * h = e
thus g * h = h * g by Def2
.= e by FUNCT_2:61 ; :: thesis: verum