set n' = n + 2;
let P1, P2 be Function of (2Set (Seg (n + 2))),the carrier of K; :: thesis: ( ( for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies P1 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies P1 . {i,j} = - (1_ K) ) ) ) & ( for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies P2 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies P2 . {i,j} = - (1_ K) ) ) ) implies P1 = P2 )
assume that
A11: for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies P1 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies P1 . {i,j} = - (1_ K) ) ) and
A12: for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies P2 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies P2 . {i,j} = - (1_ K) ) ) ; :: thesis: P1 = P2
for x being set st x in 2Set (Seg (n + 2)) holds
P1 . x = P2 . x

proof

let x be set ; :: thesis: ( x in 2Set (Seg (n + 2)) implies P1 . x = P2 . x )
assume A13: x in 2Set (Seg (n + 2)) ; :: thesis: P1 . x = P2 . x
consider i, j being Nat such that
A14: ( i in Seg (n + 2) & j in Seg (n + 2) & i < j & x = {i,j} ) by A13, Th1;
perm2 is Permutation of (Seg (n + 2)) by MATRIX_2:def 11;
then A15: perm2 . i <> perm2 . j by A14, FUNCT_2:25;

now

per cases ( perm2 . i < perm2 . j or perm2 . i > perm2 . j ) by A15, XXREAL_0:1;

case perm2 . i < perm2 . j ; :: thesis: P1 . x = P2 . x

then ( P1 . {i,j} = 1_ K & P2 . {i,j} = 1_ K ) by A11, A12, A14;
hence P1 . x = P2 . x by A14; :: thesis: verum

end;

case perm2 . i > perm2 . j ; :: thesis: P1 . x = P2 . x

then ( P1 . {i,j} = - (1_ K) & P2 . {i,j} = - (1_ K) ) by A11, A12, A14;
hence P1 . x = P2 . x by A14; :: thesis: verum

end;

end;

end;

hence P1 . x = P2 . x ; :: thesis: verum

end;

hence P1 = P2 by FUNCT_2:18; :: thesis: verum