let n be Nat; :: thesis: for K being Field
for p2, q2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j holds
(Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j}
let K be Field; :: thesis: for p2, q2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j holds
(Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j}
let p2, q2 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 & p2 . i = q2 . i & p2 . j = q2 . j holds
(Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j}
set n2 = n + 2;
let i, j be Nat; :: thesis: ( i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j implies (Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j} )
assume that
A1: ( i in Seg (n + 2) & j in Seg (n + 2) & i < j ) and
A2: ( p2 . i = q2 . i & p2 . j = q2 . j ) ; :: thesis: (Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j}
reconsider p2' = p2 as Permutation of (Seg (n + 2)) by MATRIX_2:def 11;
A3: p2' . i <> p2' . j by A1, FUNCT_2:25;

now

per cases ( p2 . i < p2 . j or p2 . i > p2 . j ) by A3, XXREAL_0:1;

suppose p2 . i < p2 . j ; :: thesis: (Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j}

then ( (Part_sgn p2,K) . {i,j} = 1_ K & (Part_sgn q2,K) . {i,j} = 1_ K ) by A1, A2, Def1;
hence (Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j} ; :: thesis: verum

end;

suppose p2 . i > p2 . j ; :: thesis: (Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j}

then ( (Part_sgn p2,K) . {i,j} = - (1_ K) & (Part_sgn q2,K) . {i,j} = - (1_ K) ) by A1, A2, Def1;
hence (Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j} ; :: thesis: verum

end;

end;

end;

hence (Part_sgn p2,K) . {i,j} = (Part_sgn q2,K) . {i,j} ; :: thesis: verum