let n be Nat; :: thesis: for K being commutative Ring st not K is degenerated & K is domRing-like holds
for p2, q2 being Element of Permutations (n + 2) st q2 = p2 " holds
sgn (p2,K) = sgn (q2,K)
let K be commutative Ring; :: thesis: ( not K is degenerated & K is domRing-like implies for p2, q2 being Element of Permutations (n + 2) st q2 = p2 " holds
sgn (p2,K) = sgn (q2,K) )
assume A0: ( not K is degenerated & K is domRing-like ) ; :: 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:6;
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 A0, Th26;
- ((1_ K),p2) = (sgn (p2,K)) * (1_ K) by Th26, A0;
then (sgn (p2,K)) * (1_ K) = sgn (q2,K) by A2, A3, VECTSP_1:def 4;
hence sgn (p2,K) = sgn (q2,K) ; :: thesis: verum