let n be Nat; :: thesis: for K being commutative Ring
for p2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & 1_ K <> - (1_ K) holds
( ( (Part_sgn (p2,K)) . {i,j} = 1_ K implies p2 . i < p2 . j ) & ( (Part_sgn (p2,K)) . {i,j} = - (1_ K) implies p2 . i > p2 . j ) )
let K be commutative Ring; :: thesis: for p2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & 1_ K <> - (1_ K) holds
( ( (Part_sgn (p2,K)) . {i,j} = 1_ K implies p2 . i < p2 . j ) & ( (Part_sgn (p2,K)) . {i,j} = - (1_ K) implies p2 . i > p2 . j ) )
let p2 be Element of Permutations (n + 2); :: thesis: for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & 1_ K <> - (1_ K) holds
( ( (Part_sgn (p2,K)) . {i,j} = 1_ K implies p2 . i < p2 . j ) & ( (Part_sgn (p2,K)) . {i,j} = - (1_ K) implies p2 . i > p2 . j ) )
set n2 = n + 2;
let i, j be Nat; :: thesis: ( i in Seg (n + 2) & j in Seg (n + 2) & i < j & 1_ K <> - (1_ K) implies ( ( (Part_sgn (p2,K)) . {i,j} = 1_ K implies p2 . i < p2 . j ) & ( (Part_sgn (p2,K)) . {i,j} = - (1_ K) implies p2 . i > p2 . j ) ) )
assume that
A1: i in Seg (n + 2) and
A2: j in Seg (n + 2) and
A3: i < j and
A4: 1_ K <> - (1_ K) ; :: thesis: ( ( (Part_sgn (p2,K)) . {i,j} = 1_ K implies p2 . i < p2 . j ) & ( (Part_sgn (p2,K)) . {i,j} = - (1_ K) implies p2 . i > p2 . j ) )
reconsider p9 = p2 as Permutation of (Seg (n + 2)) by MATRIX_1:def 12;
p9 . i <> p9 . j by A1, A2, A3, FUNCT_2:19;
then A5: ( p2 . i < p2 . j or p2 . i > p2 . j ) by XXREAL_0:1;
thus ( (Part_sgn (p2,K)) . {i,j} = 1_ K implies p2 . i < p2 . j ) :: thesis: ( (Part_sgn (p2,K)) . {i,j} = - (1_ K) implies p2 . i > p2 . j ) assume (Part_sgn (p2,K)) . {i,j} = - (1_ K) ; :: thesis: p2 . i > p2 . j
hence p2 . i > p2 . j by A1, A2, A3, A4, A5, Def1; :: thesis: verum