for n being Nat
for K being commutative Ring
for P being FinSequence of (Group_of_Perm (n + 2))
for p2 being Element of Permutations (n + 2) st p2 = Product P & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ) holds
( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )