set n9 = n + 2;
defpred S₁[ object , object ] 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 object st x in 2Set (Seg (n + 2)) holds
ex y being object st
( y in the carrier of K & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in 2Set (Seg (n + 2)) implies ex y being object st
( y in the carrier of K & S₁[x,y] ) )
assume x in 2Set (Seg (n + 2)) ; :: thesis: ex y being object 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_1:def 12;
then A6: perm2 . i <> perm2 . j by A2, A3, A4, FUNCT_2:19;

now :: thesis: ( ( perm2 . i < perm2 . j & ex y being object st
( y in the carrier of K & S₁[x,y] ) ) or ( perm2 . i > perm2 . j & ex y being object st
( y in the carrier of K & S₁[x,y] ) ) )

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 object st
( y in the carrier of K & S₁[x,y] )

S₁[x, 1_ K]

proof

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

end;

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

end;

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

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

proof

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

end;

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

end;

end;

end;

hence ex y being object 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 object 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 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 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