let n be Nat; :: thesis: for K being commutative Ring
for p2, q2, pq2 being Element of Permutations (n + 2)
for i, j being Nat st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j holds
for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn (p2,K)) . s <> (Part_sgn (pq2,K)) . s or i in s or j in s )
let K be commutative Ring; :: thesis: for p2, q2, pq2 being Element of Permutations (n + 2)
for i, j being Nat st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j holds
for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn (p2,K)) . s <> (Part_sgn (pq2,K)) . s or i in s or j in s )
set n2 = n + 2;
let p, q, pq be Element of Permutations (n + 2); :: thesis: for i, j being Nat st pq = p * q & q is being_transposition & q . i = j & i < j holds
for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn (p,K)) . s <> (Part_sgn (pq,K)) . s or i in s or j in s )
let i, j be Nat; :: thesis: ( pq = p * q & q is being_transposition & q . i = j & i < j implies for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn (p,K)) . s <> (Part_sgn (pq,K)) . s or i in s or j in s ) )
assume that
A1: pq = p * q and
A2: q is being_transposition and
A3: q . i = j and
A4: i < j ; :: thesis: for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn (p,K)) . s <> (Part_sgn (pq,K)) . s or i in s or j in s )
reconsider q9 = q, pq9 = pq as Permutation of (Seg (n + 2)) by MATRIX_1:def 12;
let s be Element of 2Set (Seg (n + 2)); :: thesis: ( not (Part_sgn (p,K)) . s <> (Part_sgn (pq,K)) . s or i in s or j in s )
assume A5: (Part_sgn (p,K)) . s <> (Part_sgn (pq,K)) . s ; :: thesis: ( i in s or j in s )
A6: dom q9 = Seg (n + 2) by FUNCT_2:52;
A7: dom pq9 = Seg (n + 2) by FUNCT_2:52;
assume that
A8: not i in s and
A9: not j in s ; :: thesis: contradiction
consider i9, j9 being Nat such that
A10: i9 in Seg (n + 2) and
A11: j9 in Seg (n + 2) and
A12: i9 < j9 and
A13: s = {i9,j9} by Th1;
A14: j <> j9 by A13, A9, TARSKI:def 2;
A15: j <> i9 by A13, A9, TARSKI:def 2;
i <> j9 by A13, A8, TARSKI:def 2;
then q . j9 = j9 by A2, A3, A4, A11, A14, A6, Th8;
then A16: pq . j9 = p . j9 by A1, A11, A7, FUNCT_1:12;
i <> i9 by A13, A8, TARSKI:def 2;
then q . i9 = i9 by A2, A3, A4, A10, A15, A6, Th8;
then pq . i9 = p . i9 by A1, A10, A7, FUNCT_1:12;
hence contradiction by A5, A10, A11, A12, A13, A16, Th6; :: thesis: verum