let n be Nat; 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; ( 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 )
; 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); ( q2 = p2 " implies sgn (p2,K) = sgn (q2,K) )
assume
q2 = p2 "
; 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)
; verum