let n be Nat; :: thesis: id (Seg n) is even
set l = <*> the carrier of (Group_of_Perm n);
0 = (2 * 0) + 0 ;
then A1: (len (<*> the carrier of (Group_of_Perm n))) mod 2 = 0 by NAT_D:def 2;
Product (<*> the carrier of (Group_of_Perm n)) = 1_ (Group_of_Perm n) by GROUP_4:8;
then A2: idseq n = Product (<*> the carrier of (Group_of_Perm n)) by Th9;
for i being Nat st i in dom (<*> the carrier of (Group_of_Perm n)) holds
ex q being Element of Permutations n st
( (<*> the carrier of (Group_of_Perm n)) . i = q & q is being_transposition ) ;
hence id (Seg n) is even by A1, A2; :: thesis: verum