let n be Nat; :: thesis: id (Seg n) is even
set l = <*> the carrier of (Group_of_Perm n);
0 mod 2 = 0

proof

0 = (2 * 0 ) + 0 ;
hence 0 mod 2 = 0 by NAT_D:def 2; :: thesis: verum

end;

then A1: (len (<*> the carrier of (Group_of_Perm n))) mod 2 = 0 ;
Product (<*> the carrier of (Group_of_Perm n)) = 1_ (Group_of_Perm n) by GROUP_4:11;
then A2: idseq n = Product (<*> the carrier of (Group_of_Perm n)) by Th28;
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 ) by RELAT_1:60;
hence id (Seg n) is even by A1, A2, Def15; :: thesis: verum