let n be Nat; :: thesis: for K being commutative Ring
for p2 being Element of Permutations (n + 2)
for s being Element of 2Set (Seg (n + 2)) holds
( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) )
let K be commutative Ring; :: thesis: for p2 being Element of Permutations (n + 2)
for s being Element of 2Set (Seg (n + 2)) holds
( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) )
let p2 be Element of Permutations (n + 2); :: thesis: for s being Element of 2Set (Seg (n + 2)) holds
( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) )
let s be Element of 2Set (Seg (n + 2)); :: thesis: ( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) )
consider i, j being Nat such that
A1: i in Seg (n + 2) and
A2: j in Seg (n + 2) and
A3: i < j and
A4: s = {i,j} by Th1;
p2 is Permutation of (Seg (n + 2)) by MATRIX_1:def 12;
then p2 . i <> p2 . j by A1, A2, A3, FUNCT_2:19;
then ( p2 . i > p2 . j or p2 . i < p2 . j ) by XXREAL_0:1;
hence ( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) ) by A1, A2, A3, A4, Def1; :: thesis: verum