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

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 b_{1} being Element of the carrier of (SymGroup X) holds

( b_{1} * e = b_{1} & e * b_{1} = b_{1} & ex b_{2} being Element of the carrier of (SymGroup X) st

( b_{1} * b_{2} = e & b_{2} * b_{1} = e ) )

let h be Element of (SymGroup X); :: thesis: ( h * e = h & e * h = h & ex b_{1} being Element of the carrier of (SymGroup X) st

( h * b_{1} = e & b_{1} * 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 b_{1} being Element of the carrier of (SymGroup X) st

( h * b_{1} = e & b_{1} * h = e ) )

thus e * h = h1 * e by Def2

.= h by FUNCT_2:17 ; :: thesis: ex b_{1} being Element of the carrier of (SymGroup X) st

( h * b_{1} = e & b_{1} * 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

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

set e = id X;
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;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

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 b

( b

( b

let h be Element of (SymGroup X); :: thesis: ( h * e = h & e * h = h & ex b

( h * b

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 b

( h * b

thus e * h = h1 * e by Def2

.= h by FUNCT_2:17 ; :: thesis: ex b

( h * b

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