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

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