set j = perm . i;

set P = Permutations n;

set p = perm;

set n1 = n + 1;

reconsider N = n as Element of NAT by ORDINAL1:def 12;

reconsider p9 = perm as Permutation of (Seg (n + 1)) by MATRIX_1:def 12;

A2: dom p9 = Seg (n + 1) by FUNCT_2:52;

defpred S_{1}[ object , object ] means for k being Nat st k in Seg n & $1 = k holds

( ( k < i implies ( ( perm . k < perm . i implies $2 = perm . k ) & ( perm . k >= perm . i implies $2 = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies $2 = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies $2 = (perm . (k + 1)) - 1 ) ) ) );

A3: rng p9 = Seg (n + 1) by FUNCT_2:def 3;

then A4: perm . i in Seg (n + 1) by A1, A2, FUNCT_1:def 3;

A5: for k9 being object st k9 in Seg n holds

ex y being object st

( y in Seg n & S_{1}[k9,y] )

A31: for x being object st x in Seg n holds

S_{1}[x,q . x]
from FUNCT_2:sch 1(A5);

for x1, x2 being object st x1 in dom q & x2 in dom q & q . x1 = q . x2 holds

x1 = x2

card (finSeg N) = card (finSeg N) ;

then ( q is one-to-one & q is onto ) by A70, FINSEQ_4:63;

then reconsider q = q as Element of Permutations n by MATRIX_1:def 12;

take q ; :: thesis: for k being Nat st k in Seg n holds

( ( k < i implies ( ( perm . k < perm . i implies q . k = perm . k ) & ( perm . k >= perm . i implies q . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q . k = (perm . (k + 1)) - 1 ) ) ) )

thus for k being Nat st k in Seg n holds

( ( k < i implies ( ( perm . k < perm . i implies q . k = perm . k ) & ( perm . k >= perm . i implies q . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q . k = (perm . (k + 1)) - 1 ) ) ) ) by A31; :: thesis: verum

set P = Permutations n;

set p = perm;

set n1 = n + 1;

reconsider N = n as Element of NAT by ORDINAL1:def 12;

reconsider p9 = perm as Permutation of (Seg (n + 1)) by MATRIX_1:def 12;

A2: dom p9 = Seg (n + 1) by FUNCT_2:52;

defpred S

( ( k < i implies ( ( perm . k < perm . i implies $2 = perm . k ) & ( perm . k >= perm . i implies $2 = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies $2 = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies $2 = (perm . (k + 1)) - 1 ) ) ) );

A3: rng p9 = Seg (n + 1) by FUNCT_2:def 3;

then A4: perm . i in Seg (n + 1) by A1, A2, FUNCT_1:def 3;

A5: for k9 being object st k9 in Seg n holds

ex y being object st

( y in Seg n & S

proof

consider q being Function of (Seg n),(Seg n) such that
let k9 be object ; :: thesis: ( k9 in Seg n implies ex y being object st

( y in Seg n & S_{1}[k9,y] ) )

assume k9 in Seg n ; :: thesis: ex y being object st

( y in Seg n & S_{1}[k9,y] )

then consider k being Nat such that

A6: k9 = k and

A7: 1 <= k and

A8: k <= n ;

A9: k < n + 1 by A8, NAT_1:13;

then A10: k in Seg (n + 1) by A7;

then A11: perm . k in Seg (n + 1) by A2, A3, FUNCT_1:def 3;

set k1 = k + 1;

A12: 1 + 0 <= k + 1 by NAT_1:13;

k + 1 <= n + 1 by A9, NAT_1:13;

then A13: k + 1 in Seg (n + 1) by A12;

then A14: perm . (k + 1) in Seg (n + 1) by A2, A3, FUNCT_1:def 3;

end;( y in Seg n & S

assume k9 in Seg n ; :: thesis: ex y being object st

( y in Seg n & S

then consider k being Nat such that

A6: k9 = k and

A7: 1 <= k and

A8: k <= n ;

A9: k < n + 1 by A8, NAT_1:13;

then A10: k in Seg (n + 1) by A7;

then A11: perm . k in Seg (n + 1) by A2, A3, FUNCT_1:def 3;

set k1 = k + 1;

A12: 1 + 0 <= k + 1 by NAT_1:13;

k + 1 <= n + 1 by A9, NAT_1:13;

then A13: k + 1 in Seg (n + 1) by A12;

then A14: perm . (k + 1) in Seg (n + 1) by A2, A3, FUNCT_1:def 3;

per cases
( ( k < i & perm . k < perm . i ) or ( k < i & perm . k >= perm . i ) or ( k >= i & perm . (k + 1) < perm . i ) or ( k >= i & perm . (k + 1) >= perm . i ) )
;

end;

suppose A15:
( k < i & perm . k < perm . i )
; :: thesis: ex y being object st

( y in Seg n & S_{1}[k9,y] )

( y in Seg n & S

perm . i <= n + 1
by A4, FINSEQ_1:1;

then perm . k < n + 1 by A15, XXREAL_0:2;

then A16: perm . k <= n by NAT_1:13;

A17: S_{1}[k9,perm . k]
by A6, A15;

1 <= perm . k by A11, FINSEQ_1:1;

then perm . k in Seg n by A16;

hence ex y being object st

( y in Seg n & S_{1}[k9,y] )
by A17; :: thesis: verum

end;then perm . k < n + 1 by A15, XXREAL_0:2;

then A16: perm . k <= n by NAT_1:13;

A17: S

1 <= perm . k by A11, FINSEQ_1:1;

then perm . k in Seg n by A16;

hence ex y being object st

( y in Seg n & S

suppose A18:
( k < i & perm . k >= perm . i )
; :: thesis: ex y being object st

( y in Seg n & S_{1}[k9,y] )

( y in Seg n & S

then
p9 . k <> p9 . i
by A1, A10, FUNCT_2:19;

then A19: perm . k > perm . i by A18, XXREAL_0:1;

then reconsider pk1 = (perm . k) - 1 as Element of NAT by NAT_1:20;

A20: S_{1}[k9,pk1]
by A6, A18;

A21: pk1 < pk1 + 1 by NAT_1:13;

perm . k <= n + 1 by A11, FINSEQ_1:1;

then pk1 < n + 1 by A21, XXREAL_0:2;

then A22: pk1 <= n by NAT_1:13;

perm . i >= 1 by A4, FINSEQ_1:1;

then pk1 + 1 > 1 by A19, XXREAL_0:2;

then pk1 >= 1 by NAT_1:13;

then pk1 in Seg n by A22;

hence ex y being object st

( y in Seg n & S_{1}[k9,y] )
by A20; :: thesis: verum

end;then A19: perm . k > perm . i by A18, XXREAL_0:1;

then reconsider pk1 = (perm . k) - 1 as Element of NAT by NAT_1:20;

A20: S

A21: pk1 < pk1 + 1 by NAT_1:13;

perm . k <= n + 1 by A11, FINSEQ_1:1;

then pk1 < n + 1 by A21, XXREAL_0:2;

then A22: pk1 <= n by NAT_1:13;

perm . i >= 1 by A4, FINSEQ_1:1;

then pk1 + 1 > 1 by A19, XXREAL_0:2;

then pk1 >= 1 by NAT_1:13;

then pk1 in Seg n by A22;

hence ex y being object st

( y in Seg n & S

suppose A23:
( k >= i & perm . (k + 1) < perm . i )
; :: thesis: ex y being object st

( y in Seg n & S_{1}[k9,y] )

( y in Seg n & S

perm . i <= n + 1
by A4, FINSEQ_1:1;

then perm . (k + 1) < n + 1 by A23, XXREAL_0:2;

then A24: perm . (k + 1) <= n by NAT_1:13;

A25: S_{1}[k9,perm . (k + 1)]
by A6, A23;

1 <= perm . (k + 1) by A14, FINSEQ_1:1;

then perm . (k + 1) in Seg n by A24;

hence ex y being object st

( y in Seg n & S_{1}[k9,y] )
by A25; :: thesis: verum

end;then perm . (k + 1) < n + 1 by A23, XXREAL_0:2;

then A24: perm . (k + 1) <= n by NAT_1:13;

A25: S

1 <= perm . (k + 1) by A14, FINSEQ_1:1;

then perm . (k + 1) in Seg n by A24;

hence ex y being object st

( y in Seg n & S

suppose A26:
( k >= i & perm . (k + 1) >= perm . i )
; :: thesis: ex y being object st

( y in Seg n & S_{1}[k9,y] )

( y in Seg n & S

then
i < k + 1
by NAT_1:13;

then p9 . (k + 1) <> p9 . i by A1, A13, FUNCT_2:19;

then A27: perm . (k + 1) > perm . i by A26, XXREAL_0:1;

then reconsider pk1 = (perm . (k + 1)) - 1 as Element of NAT by NAT_1:20;

A28: S_{1}[k9,pk1]
by A6, A26;

A29: pk1 < pk1 + 1 by NAT_1:13;

perm . (k + 1) <= n + 1 by A14, FINSEQ_1:1;

then pk1 < n + 1 by A29, XXREAL_0:2;

then A30: pk1 <= n by NAT_1:13;

perm . i >= 1 by A4, FINSEQ_1:1;

then pk1 + 1 > 1 by A27, XXREAL_0:2;

then pk1 >= 1 by NAT_1:13;

then pk1 in Seg n by A30;

hence ex y being object st

( y in Seg n & S_{1}[k9,y] )
by A28; :: thesis: verum

end;then p9 . (k + 1) <> p9 . i by A1, A13, FUNCT_2:19;

then A27: perm . (k + 1) > perm . i by A26, XXREAL_0:1;

then reconsider pk1 = (perm . (k + 1)) - 1 as Element of NAT by NAT_1:20;

A28: S

A29: pk1 < pk1 + 1 by NAT_1:13;

perm . (k + 1) <= n + 1 by A14, FINSEQ_1:1;

then pk1 < n + 1 by A29, XXREAL_0:2;

then A30: pk1 <= n by NAT_1:13;

perm . i >= 1 by A4, FINSEQ_1:1;

then pk1 + 1 > 1 by A27, XXREAL_0:2;

then pk1 >= 1 by NAT_1:13;

then pk1 in Seg n by A30;

hence ex y being object st

( y in Seg n & S

A31: for x being object st x in Seg n holds

S

for x1, x2 being object st x1 in dom q & x2 in dom q & q . x1 = q . x2 holds

x1 = x2

proof

then A70:
q is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom q & x2 in dom q & q . x1 = q . x2 implies x1 = x2 )

assume that

A32: x1 in dom q and

A33: x2 in dom q and

A34: q . x1 = q . x2 ; :: thesis: x1 = x2

A35: dom q = Seg n by FUNCT_2:52;

then consider k1 being Nat such that

A36: x1 = k1 and

A37: 1 <= k1 and

A38: k1 <= n by A32;

A39: 0 + 1 <= k1 + 1 by NAT_1:13;

A40: k1 < n + 1 by A38, NAT_1:13;

then A41: k1 in Seg (n + 1) by A37;

k1 + 1 <= n + 1 by A40, NAT_1:13;

then A42: k1 + 1 in Seg (n + 1) by A39;

consider k2 being Nat such that

A43: x2 = k2 and

A44: 1 <= k2 and

A45: k2 <= n by A33, A35;

A46: k2 < n + 1 by A45, NAT_1:13;

then A47: k2 in Seg (n + 1) by A44;

A48: 0 + 1 <= k2 + 1 by NAT_1:13;

k2 + 1 <= n + 1 by A46, NAT_1:13;

then A49: k2 + 1 in Seg (n + 1) by A48;

end;assume that

A32: x1 in dom q and

A33: x2 in dom q and

A34: q . x1 = q . x2 ; :: thesis: x1 = x2

A35: dom q = Seg n by FUNCT_2:52;

then consider k1 being Nat such that

A36: x1 = k1 and

A37: 1 <= k1 and

A38: k1 <= n by A32;

A39: 0 + 1 <= k1 + 1 by NAT_1:13;

A40: k1 < n + 1 by A38, NAT_1:13;

then A41: k1 in Seg (n + 1) by A37;

k1 + 1 <= n + 1 by A40, NAT_1:13;

then A42: k1 + 1 in Seg (n + 1) by A39;

consider k2 being Nat such that

A43: x2 = k2 and

A44: 1 <= k2 and

A45: k2 <= n by A33, A35;

A46: k2 < n + 1 by A45, NAT_1:13;

then A47: k2 in Seg (n + 1) by A44;

A48: 0 + 1 <= k2 + 1 by NAT_1:13;

k2 + 1 <= n + 1 by A46, NAT_1:13;

then A49: k2 + 1 in Seg (n + 1) by A48;

per cases
( ( k1 < i & perm . k1 < perm . i ) or ( k1 < i & perm . k1 >= perm . i ) or ( k1 >= i & perm . (k1 + 1) < perm . i ) or ( k1 >= i & perm . (k1 + 1) >= perm . i ) )
;

end;

suppose A50:
( k1 < i & perm . k1 < perm . i )
; :: thesis: x1 = x2

then A51:
q . k1 = p9 . k1
by A31, A32, A36;

end;per cases
( ( k2 < i & perm . k2 < perm . i ) or ( k2 < i & perm . k2 >= perm . i ) or ( k2 >= i & perm . (k2 + 1) < perm . i ) or ( k2 >= i & perm . (k2 + 1) >= perm . i ) )
;

end;

suppose
( k2 < i & perm . k2 < perm . i )
; :: thesis: x1 = x2

then
p9 . k2 = p9 . k1
by A31, A33, A34, A36, A43, A51;

hence x1 = x2 by A2, A36, A43, A41, A47, FUNCT_1:def 4; :: thesis: verum

end;hence x1 = x2 by A2, A36, A43, A41, A47, FUNCT_1:def 4; :: thesis: verum

suppose A52:
( k2 < i & perm . k2 >= perm . i )
; :: thesis: x1 = x2

then
q . k2 = (perm . k2) - 1
by A31, A33, A43;

then (perm . k1) + 1 = perm . k2 by A34, A36, A43, A51;

then perm . k2 <= perm . i by A50, NAT_1:13;

then p9 . k2 = p9 . i by A52, XXREAL_0:1;

hence x1 = x2 by A1, A2, A47, A52, FUNCT_1:def 4; :: thesis: verum

end;then (perm . k1) + 1 = perm . k2 by A34, A36, A43, A51;

then perm . k2 <= perm . i by A50, NAT_1:13;

then p9 . k2 = p9 . i by A52, XXREAL_0:1;

hence x1 = x2 by A1, A2, A47, A52, FUNCT_1:def 4; :: thesis: verum

suppose A53:
( k2 >= i & perm . (k2 + 1) < perm . i )
; :: thesis: x1 = x2

then
p9 . k1 = p9 . (k2 + 1)
by A31, A33, A34, A36, A43, A51;

then k1 = k2 + 1 by A2, A41, A49, FUNCT_1:def 4;

hence x1 = x2 by A50, A53, NAT_1:13; :: thesis: verum

end;then k1 = k2 + 1 by A2, A41, A49, FUNCT_1:def 4;

hence x1 = x2 by A50, A53, NAT_1:13; :: thesis: verum

suppose A54:
( k2 >= i & perm . (k2 + 1) >= perm . i )
; :: thesis: x1 = x2

then
perm . k1 = (perm . (k2 + 1)) - 1
by A31, A33, A34, A36, A43, A51;

then (perm . k1) + 1 = perm . (k2 + 1) ;

then perm . (k2 + 1) <= perm . i by A50, NAT_1:13;

then p9 . (k2 + 1) = perm . i by A54, XXREAL_0:1;

then k2 + 1 = i by A1, A2, A49, FUNCT_1:def 4;

hence x1 = x2 by A54, NAT_1:13; :: thesis: verum

end;then (perm . k1) + 1 = perm . (k2 + 1) ;

then perm . (k2 + 1) <= perm . i by A50, NAT_1:13;

then p9 . (k2 + 1) = perm . i by A54, XXREAL_0:1;

then k2 + 1 = i by A1, A2, A49, FUNCT_1:def 4;

hence x1 = x2 by A54, NAT_1:13; :: thesis: verum

suppose A55:
( k1 < i & perm . k1 >= perm . i )
; :: thesis: x1 = x2

then A56:
q . k1 = (perm . k1) - 1
by A31, A32, A36;

end;per cases
( ( k2 < i & perm . k2 < perm . i ) or ( k2 < i & perm . k2 >= perm . i ) or ( k2 >= i & perm . (k2 + 1) < perm . i ) or ( k2 >= i & perm . (k2 + 1) >= perm . i ) )
;

end;

suppose A57:
( k2 < i & perm . k2 < perm . i )
; :: thesis: x1 = x2

then
q . k2 = p9 . k2
by A31, A33, A43;

then perm . k1 = (perm . k2) + 1 by A34, A36, A43, A56;

then perm . k1 <= perm . i by A57, NAT_1:13;

then perm . k1 = perm . i by A55, XXREAL_0:1;

hence x1 = x2 by A1, A2, A41, A55, FUNCT_1:def 4; :: thesis: verum

end;then perm . k1 = (perm . k2) + 1 by A34, A36, A43, A56;

then perm . k1 <= perm . i by A57, NAT_1:13;

then perm . k1 = perm . i by A55, XXREAL_0:1;

hence x1 = x2 by A1, A2, A41, A55, FUNCT_1:def 4; :: thesis: verum

suppose
( k2 < i & perm . k2 >= perm . i )
; :: thesis: x1 = x2

then
(perm . k1) - 1 = (perm . k2) - 1
by A31, A33, A34, A36, A43, A56;

hence x1 = x2 by A2, A36, A43, A41, A47, FUNCT_1:def 4; :: thesis: verum

end;hence x1 = x2 by A2, A36, A43, A41, A47, FUNCT_1:def 4; :: thesis: verum

suppose A58:
( k2 >= i & perm . (k2 + 1) < perm . i )
; :: thesis: x1 = x2

then
(perm . k1) - 1 = perm . (k2 + 1)
by A31, A33, A34, A36, A43, A56;

then (perm . (k2 + 1)) + 1 = perm . k1 ;

then perm . k1 <= perm . i by A58, NAT_1:13;

then p9 . k1 = p9 . i by A55, XXREAL_0:1;

hence x1 = x2 by A1, A2, A41, A55, FUNCT_1:def 4; :: thesis: verum

end;then (perm . (k2 + 1)) + 1 = perm . k1 ;

then perm . k1 <= perm . i by A58, NAT_1:13;

then p9 . k1 = p9 . i by A55, XXREAL_0:1;

hence x1 = x2 by A1, A2, A41, A55, FUNCT_1:def 4; :: thesis: verum

suppose A60:
( k1 >= i & perm . (k1 + 1) < perm . i )
; :: thesis: x1 = x2

then A61:
q . k1 = perm . (k1 + 1)
by A31, A32, A36;

end;per cases
( ( k2 < i & perm . k2 < perm . i ) or ( k2 < i & perm . k2 >= perm . i ) or ( k2 >= i & perm . (k2 + 1) < perm . i ) or ( k2 >= i & perm . (k2 + 1) >= perm . i ) )
;

end;

suppose A62:
( k2 < i & perm . k2 < perm . i )
; :: thesis: x1 = x2

then
p9 . (k1 + 1) = p9 . k2
by A31, A33, A34, A36, A43, A61;

then k1 + 1 = k2 by A2, A47, A42, FUNCT_1:def 4;

hence x1 = x2 by A60, A62, NAT_1:13; :: thesis: verum

end;then k1 + 1 = k2 by A2, A47, A42, FUNCT_1:def 4;

hence x1 = x2 by A60, A62, NAT_1:13; :: thesis: verum

suppose A63:
( k2 < i & perm . k2 >= perm . i )
; :: thesis: x1 = x2

then
perm . (k1 + 1) = (perm . k2) - 1
by A31, A33, A34, A36, A43, A61;

then perm . k2 = (perm . (k1 + 1)) + 1 ;

then perm . k2 <= perm . i by A60, NAT_1:13;

then p9 . k2 = p9 . i by A63, XXREAL_0:1;

hence x1 = x2 by A1, A2, A47, A63, FUNCT_1:def 4; :: thesis: verum

end;then perm . k2 = (perm . (k1 + 1)) + 1 ;

then perm . k2 <= perm . i by A60, NAT_1:13;

then p9 . k2 = p9 . i by A63, XXREAL_0:1;

hence x1 = x2 by A1, A2, A47, A63, FUNCT_1:def 4; :: thesis: verum

suppose
( k2 >= i & perm . (k2 + 1) < perm . i )
; :: thesis: x1 = x2

then
q . k2 = perm . (k2 + 1)
by A31, A33, A43;

then k1 + 1 = k2 + 1 by A2, A34, A36, A43, A42, A49, A61, FUNCT_1:def 4;

hence x1 = x2 by A36, A43; :: thesis: verum

end;then k1 + 1 = k2 + 1 by A2, A34, A36, A43, A42, A49, A61, FUNCT_1:def 4;

hence x1 = x2 by A36, A43; :: thesis: verum

suppose A64:
( k2 >= i & perm . (k2 + 1) >= perm . i )
; :: thesis: x1 = x2

then
perm . (k1 + 1) = (perm . (k2 + 1)) - 1
by A31, A33, A34, A36, A43, A61;

then perm . (k2 + 1) = (perm . (k1 + 1)) + 1 ;

then perm . (k2 + 1) <= perm . i by A60, NAT_1:13;

then p9 . (k2 + 1) = p9 . i by A64, XXREAL_0:1;

then k2 + 1 = i by A1, A2, A49, FUNCT_1:def 4;

hence x1 = x2 by A64, NAT_1:13; :: thesis: verum

end;then perm . (k2 + 1) = (perm . (k1 + 1)) + 1 ;

then perm . (k2 + 1) <= perm . i by A60, NAT_1:13;

then p9 . (k2 + 1) = p9 . i by A64, XXREAL_0:1;

then k2 + 1 = i by A1, A2, A49, FUNCT_1:def 4;

hence x1 = x2 by A64, NAT_1:13; :: thesis: verum

suppose A65:
( k1 >= i & perm . (k1 + 1) >= perm . i )
; :: thesis: x1 = x2

then A66:
q . k1 = (perm . (k1 + 1)) - 1
by A31, A32, A36;

end;per cases
( ( k2 < i & perm . k2 < perm . i ) or ( k2 < i & perm . k2 >= perm . i ) or ( k2 >= i & perm . (k2 + 1) < perm . i ) or ( k2 >= i & perm . (k2 + 1) >= perm . i ) )
;

end;

suppose A67:
( k2 < i & perm . k2 < perm . i )
; :: thesis: x1 = x2

then
(perm . (k1 + 1)) - 1 = perm . k2
by A31, A33, A34, A36, A43, A66;

then perm . (k1 + 1) = (perm . k2) + 1 ;

then perm . (k1 + 1) <= perm . i by A67, NAT_1:13;

then p9 . (k1 + 1) = p9 . i by A65, XXREAL_0:1;

then k1 + 1 = i by A1, A2, A42, FUNCT_1:def 4;

hence x1 = x2 by A65, NAT_1:13; :: thesis: verum

end;then perm . (k1 + 1) = (perm . k2) + 1 ;

then perm . (k1 + 1) <= perm . i by A67, NAT_1:13;

then p9 . (k1 + 1) = p9 . i by A65, XXREAL_0:1;

then k1 + 1 = i by A1, A2, A42, FUNCT_1:def 4;

hence x1 = x2 by A65, NAT_1:13; :: thesis: verum

suppose A68:
( k2 < i & perm . k2 >= perm . i )
; :: thesis: x1 = x2

then
(perm . (k1 + 1)) - 1 = (perm . k2) - 1
by A31, A33, A34, A36, A43, A66;

then k1 + 1 = k2 by A2, A47, A42, FUNCT_1:def 4;

hence x1 = x2 by A65, A68, NAT_1:13; :: thesis: verum

end;then k1 + 1 = k2 by A2, A47, A42, FUNCT_1:def 4;

hence x1 = x2 by A65, A68, NAT_1:13; :: thesis: verum

suppose A69:
( k2 >= i & perm . (k2 + 1) < perm . i )
; :: thesis: x1 = x2

then
(perm . (k1 + 1)) - 1 = perm . (k2 + 1)
by A31, A33, A34, A36, A43, A66;

then perm . (k1 + 1) = (perm . (k2 + 1)) + 1 ;

then perm . (k1 + 1) <= perm . i by A69, NAT_1:13;

then p9 . (k1 + 1) = p9 . i by A65, XXREAL_0:1;

then k1 + 1 = i by A1, A2, A42, FUNCT_1:def 4;

hence x1 = x2 by A65, NAT_1:13; :: thesis: verum

end;then perm . (k1 + 1) = (perm . (k2 + 1)) + 1 ;

then perm . (k1 + 1) <= perm . i by A69, NAT_1:13;

then p9 . (k1 + 1) = p9 . i by A65, XXREAL_0:1;

then k1 + 1 = i by A1, A2, A42, FUNCT_1:def 4;

hence x1 = x2 by A65, NAT_1:13; :: thesis: verum

card (finSeg N) = card (finSeg N) ;

then ( q is one-to-one & q is onto ) by A70, FINSEQ_4:63;

then reconsider q = q as Element of Permutations n by MATRIX_1:def 12;

take q ; :: thesis: for k being Nat st k in Seg n holds

( ( k < i implies ( ( perm . k < perm . i implies q . k = perm . k ) & ( perm . k >= perm . i implies q . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q . k = (perm . (k + 1)) - 1 ) ) ) )

thus for k being Nat st k in Seg n holds

( ( k < i implies ( ( perm . k < perm . i implies q . k = perm . k ) & ( perm . k >= perm . i implies q . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies q . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies q . k = (perm . (k + 1)) - 1 ) ) ) ) by A31; :: thesis: verum