set n' = n + 2;
defpred S₁[ set , set ] means for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j & $1 = {i,j} holds
( ( perm2 . i < perm2 . j implies $2 = 1_ K ) & ( perm2 . i > perm2 . j implies $2 = - (1_ K) ) );
A1: for x being set st x in 2Set (Seg (n + 2)) holds
ex y being set st
( y in the carrier of K & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in 2Set (Seg (n + 2)) implies ex y being set st
( y in the carrier of K & S₁[x,y] ) )
assume x in 2Set (Seg (n + 2)) ; :: thesis: ex y being set st
( y in the carrier of K & S₁[x,y] )
then consider i, j being Nat such that
A2: i in Seg (n + 2) and
A3: j in Seg (n + 2) and
A4: i < j and
A5: x = {i,j} by Th1;
perm2 is Permutation of Seg (n + 2) by MATRIX_2:def 11;
then A6: perm2 . i <> perm2 . j by A2, A3, A4, FUNCT_2:25;

now

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

case A7: perm2 . i < perm2 . j ; :: thesis: ex y being set st
( y in the carrier of K & S₁[x,y] )

S₁[x, 1_ K]

proof

let i', j' be Element of NAT ; :: thesis: ( i' in Seg (n + 2) & j' in Seg (n + 2) & i' < j' & x = {i',j'} implies ( ( perm2 . i' < perm2 . j' implies 1_ K = 1_ K ) & ( perm2 . i' > perm2 . j' implies 1_ K = - (1_ K) ) ) )
assume that
i' in Seg (n + 2) and
j' in Seg (n + 2) and
A8: i' < j' and
A9: x = {i',j'} ; :: thesis: ( ( perm2 . i' < perm2 . j' implies 1_ K = 1_ K ) & ( perm2 . i' > perm2 . j' implies 1_ K = - (1_ K) ) )
( ( i = i' & j = j' ) or ( i = j' & j = i' ) ) by A5, A9, ZFMISC_1:28;
hence ( ( perm2 . i' < perm2 . j' implies 1_ K = 1_ K ) & ( perm2 . i' > perm2 . j' implies 1_ K = - (1_ K) ) ) by A4, A7, A8; :: thesis: verum

end;

hence ex y being set st
( y in the carrier of K & S₁[x,y] ) ; :: thesis: verum

end;

case A10: perm2 . i > perm2 . j ; :: thesis: ex y being set st
( y in the carrier of K & S₁[x,y] )

S₁[x, - (1_ K)]

proof

let i', j' be Element of NAT ; :: thesis: ( i' in Seg (n + 2) & j' in Seg (n + 2) & i' < j' & x = {i',j'} implies ( ( perm2 . i' < perm2 . j' implies - (1_ K) = 1_ K ) & ( perm2 . i' > perm2 . j' implies - (1_ K) = - (1_ K) ) ) )
assume that
i' in Seg (n + 2) and
j' in Seg (n + 2) and
A11: i' < j' and
A12: x = {i',j'} ; :: thesis: ( ( perm2 . i' < perm2 . j' implies - (1_ K) = 1_ K ) & ( perm2 . i' > perm2 . j' implies - (1_ K) = - (1_ K) ) )
( ( i = i' & j = j' ) or ( i = j' & j = i' ) ) by A5, A12, ZFMISC_1:28;
hence ( ( perm2 . i' < perm2 . j' implies - (1_ K) = 1_ K ) & ( perm2 . i' > perm2 . j' implies - (1_ K) = - (1_ K) ) ) by A4, A10, A11; :: thesis: verum

end;

hence ex y being set st
( y in the carrier of K & S₁[x,y] ) ; :: thesis: verum

end;

end;

end;

hence ex y being set st
( y in the carrier of K & S₁[x,y] ) ; :: thesis: verum

end;

consider Path being Function of 2Set (Seg (n + 2)),the carrier of K such that
A13: for x being set st x in 2Set (Seg (n + 2)) holds
S₁[x,Path . x] from FUNCT_2:sch 1(A1);
take Path ; :: 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 Path . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies Path . {i,j} = - (1_ K) ) )
let i, j be Element of NAT ; :: thesis: ( i in Seg (n + 2) & j in Seg (n + 2) & i < j implies ( ( perm2 . i < perm2 . j implies Path . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies Path . {i,j} = - (1_ K) ) ) )
assume that
A14: i in Seg (n + 2) and
A15: j in Seg (n + 2) and
A16: i < j ; :: thesis: ( ( perm2 . i < perm2 . j implies Path . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies Path . {i,j} = - (1_ K) ) )
{i,j} in 2Set (Seg (n + 2)) by A14, A15, A16, Th1;
hence ( ( perm2 . i < perm2 . j implies Path . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies Path . {i,j} = - (1_ K) ) ) by A13, A14, A15, A16; :: thesis: verum