let n be Nat; :: thesis: SymGroup (Seg n) = Group_of_Perm n

A1: the carrier of (SymGroup (Seg n)) = permutations (Seg n) by Def2;

A2: permutations (Seg n) = Permutations n by Th3

.= the carrier of (Group_of_Perm n) by MATRIX_1:def 13 ;

A1: the carrier of (SymGroup (Seg n)) = permutations (Seg n) by Def2;

A2: permutations (Seg n) = Permutations n by Th3

.= the carrier of (Group_of_Perm n) by MATRIX_1:def 13 ;

now :: thesis: for a, b being Element of (SymGroup (Seg n)) holds the multF of (SymGroup (Seg n)) . (a,b) = the multF of (Group_of_Perm n) . (a,b)

hence
SymGroup (Seg n) = Group_of_Perm n
by A1, A2, BINOP_1:2; :: thesis: verumlet a, b be Element of (SymGroup (Seg n)); :: thesis: the multF of (SymGroup (Seg n)) . (a,b) = the multF of (Group_of_Perm n) . (a,b)

A3: a * b = b * a by Def2;

( a is Permutation of (Seg n) & b is Permutation of (Seg n) ) by Th5;

then ( a in Permutations n & b in Permutations n ) by MATRIX_1:def 12;

hence the multF of (SymGroup (Seg n)) . (a,b) = the multF of (Group_of_Perm n) . (a,b) by A3, MATRIX_1:def 13; :: thesis: verum

end;A3: a * b = b * a by Def2;

( a is Permutation of (Seg n) & b is Permutation of (Seg n) ) by Th5;

then ( a in Permutations n & b in Permutations n ) by MATRIX_1:def 12;

hence the multF of (SymGroup (Seg n)) . (a,b) = the multF of (Group_of_Perm n) . (a,b) by A3, MATRIX_1:def 13; :: thesis: verum