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 ;
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)
let 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;
hence SymGroup (Seg n) = Group_of_Perm n by A1, A2, BINOP_1:2; :: thesis: verum