set n9 = n + 2;
let P1, P2 be Function of (2Set (Seg (n + 2))), the carrier of K; :: thesis: ( ( for i, j being 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 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
A17: for i, j being 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
A18: for i, j being 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 object st x in 2Set (Seg (n + 2)) holds
P1 . x = P2 . x
proof
let x be object ; :: thesis: ( x in 2Set (Seg (n + 2)) implies P1 . x = P2 . x )
assume x in 2Set (Seg (n + 2)) ; :: thesis: P1 . x = P2 . x
then consider i, j being Nat such that
A19: i in Seg (n + 2) and
A20: j in Seg (n + 2) and
A21: i < j and
A22: x = {i,j} by Th1;
perm2 is Permutation of (Seg (n + 2)) by MATRIX_1:def 12;
then A23: perm2 . i <> perm2 . j by A19, A20, A21, FUNCT_2:19;
now :: thesis: ( ( perm2 . i < perm2 . j & P1 . x = P2 . x ) or ( perm2 . i > perm2 . j & P1 . x = P2 . x ) )
per cases ( perm2 . i < perm2 . j or perm2 . i > perm2 . j ) by A23, XXREAL_0:1;
case A24: perm2 . i < perm2 . j ; :: thesis: P1 . x = P2 . x
then P1 . {i,j} = 1_ K by A17, A19, A20, A21;
hence P1 . x = P2 . x by A18, A19, A20, A21, A22, A24; :: thesis: verum
end;
case A25: perm2 . i > perm2 . j ; :: thesis: P1 . x = P2 . x
then P1 . {i,j} = - (1_ K) by A17, A19, A20, A21;
hence P1 . x = P2 . x by A18, A19, A20, A21, A22, A25; :: thesis: verum
end;
end;
end;
hence P1 . x = P2 . x ; :: thesis: verum
end;
hence P1 = P2 by FUNCT_2:12; :: thesis: verum