let n be Nat; :: thesis: for K being Field
for p2, q2 being Element of Permutations (n + 2) st q2 = p2 " holds
sgn p2,K = sgn q2,K
let K be Field; :: thesis: for p2, q2 being Element of Permutations (n + 2) st q2 = p2 " holds
sgn p2,K = sgn q2,K
A1: (n + 1) + 1 >= 0 + 1 by XREAL_1:8;
let p2, q2 be Element of Permutations (n + 2); :: thesis: ( q2 = p2 " implies sgn p2,K = sgn q2,K )
assume q2 = p2 " ; :: thesis: sgn p2,K = sgn q2,K
then A2: - (1_ K),p2 = - (1_ K),q2 by A1, MATRIX_7:29;
A3: - (1_ K),q2 = (sgn q2,K) * (1_ K) by Th26;
- (1_ K),p2 = (sgn p2,K) * (1_ K) by Th26;
then (sgn p2,K) * (1_ K) = sgn q2,K by A2, A3, VECTSP_1:def 13;
hence sgn p2,K = sgn q2,K by VECTSP_1:def 13; :: thesis: verum