let n be Nat; 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; 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); 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; ( 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
; 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)); ( 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
; ( 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
; 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; verum