let n, q be Nat; :: thesis: ( q in Seg (n + 1) implies ex p being Permutation of (Seg (n + 1)) st
for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) )
assume A1: q in Seg (n + 1) ; :: thesis: ex p being Permutation of (Seg (n + 1)) st
for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )
defpred S₁[ Element of NAT , set ] means ( ( $1 < q implies $2 = $1 ) & ( $1 = q implies $2 = n + 1 ) & ( $1 > q implies $2 = $1 - 1 ) );
A2: for i being Element of NAT st i in Seg (n + 1) holds
ex p being Element of NAT st S₁[i,p]

proof

let i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies ex p being Element of NAT st S₁[i,p] )
assume i in Seg (n + 1) ; :: thesis: ex p being Element of NAT st S₁[i,p]

per cases ( i < q or i = q or i > q ) by XXREAL_0:1;

suppose A3: i < q ; :: thesis: ex p being Element of NAT st S₁[i,p]

take i ; :: thesis: S₁[i,i]
thus S₁[i,i] by A3; :: thesis: verum

end;

suppose A4: i = q ; :: thesis: ex p being Element of NAT st S₁[i,p]

take n + 1 ; :: thesis: S₁[i,n + 1]
thus S₁[i,n + 1] by A4; :: thesis: verum

end;

suppose A5: i > q ; :: thesis: ex p being Element of NAT st S₁[i,p]

1 <= q by A1, FINSEQ_1:3;
then reconsider p = i - 1 as Element of NAT by A5, INT_1:18, XXREAL_0:2;
take p ; :: thesis: S₁[i,p]
thus S₁[i,p] by A5; :: thesis: verum

end;

end;

end;

consider p being FinSequence of NAT such that
A6: dom p = Seg (n + 1) and
A7: for i being Element of NAT st i in Seg (n + 1) holds
S₁[i,p /. i] from POLYNOM2:sch 1(A2);
A8: for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

proof

let i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) )
assume A9: i in Seg (n + 1) ; :: thesis: ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )
then p /. i = p . i by A6, PARTFUN1:def 8;
hence ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) by A7, A9; :: thesis: verum

end;

for i being set holds
( i in rng p iff i in Seg (n + 1) )

proof

let i be set ; :: thesis: ( i in rng p iff i in Seg (n + 1) )
thus ( i in rng p implies i in Seg (n + 1) ) :: thesis: ( i in Seg (n + 1) implies i in rng p )

proof

assume i in rng p ; :: thesis: i in Seg (n + 1)
then consider j being set such that
A10: j in Seg (n + 1) and
A11: p . j = i by A6, FUNCT_1:def 5;
reconsider j = j as Element of NAT by A10;

per cases ( j < q or j = q or j > q ) by XXREAL_0:1;

suppose j < q ; :: thesis: i in Seg (n + 1)

hence i in Seg (n + 1) by A8, A10, A11; :: thesis: verum

end;

suppose j = q ; :: thesis: i in Seg (n + 1)

then i = n + 1 by A8, A10, A11;
hence i in Seg (n + 1) by FINSEQ_1:6; :: thesis: verum

end;

suppose A12: j > q ; :: thesis: i in Seg (n + 1)

then A13: i = j - 1 by A8, A10, A11;
A14: 1 <= q by A1, FINSEQ_1:3;
then reconsider i = i as Element of NAT by A12, A13, INT_1:18, XXREAL_0:2;
1 < i + 1 by A12, A13, A14, XXREAL_0:2;
then A15: 1 <= i by NAT_1:13;
j <= n + 1 by A10, FINSEQ_1:3;
then i <= n by A13, XREAL_1:22;
then i <= n + 1 by NAT_1:12;
hence i in Seg (n + 1) by A15, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

thus ( i in Seg (n + 1) implies i in rng p ) :: thesis: verum

proof

assume A16: i in Seg (n + 1) ; :: thesis: i in rng p
then reconsider i = i as Element of NAT ;
( 1 <= i & i <= n + 1 ) by A16, FINSEQ_1:3;
then A17: ( i = n + 1 or i < n + 1 ) by XXREAL_0:1;

per cases ( i < q or ( q <= i & i <= n ) or i = n + 1 ) by A17, NAT_1:13;

suppose i < q ; :: thesis: i in rng p

then p . i = i by A8, A16;
hence i in rng p by A6, A16, FUNCT_1:12; :: thesis: verum

end;

suppose A18: ( q <= i & i <= n ) ; :: thesis: i in rng p

then A19: i + 1 <= n + 1 by XREAL_1:8;
1 <= i + 1 by NAT_1:12;
then A20: i + 1 in Seg (n + 1) by A19, FINSEQ_1:3;
q < i + 1 by A18, NAT_1:13;
then p . (i + 1) = (i + 1) - 1 by A8, A20
.= i ;
hence i in rng p by A6, A20, FUNCT_1:12; :: thesis: verum

end;

suppose i = n + 1 ; :: thesis: i in rng p

then p . q = i by A1, A8;
hence i in rng p by A1, A6, FUNCT_1:12; :: thesis: verum

end;

end;

end;

end;

then A21: rng p = Seg (n + 1) by TARSKI:2;
A22: for i being Element of NAT st i in Seg (n + 1) holds
( i = q iff p /. i = n + 1 )

proof

let i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies ( i = q iff p /. i = n + 1 ) )
assume A23: i in Seg (n + 1) ; :: thesis: ( i = q iff p /. i = n + 1 )
hence ( i = q implies p /. i = n + 1 ) by A7; :: thesis: ( p /. i = n + 1 implies i = q )
thus ( p /. i = n + 1 implies i = q ) :: thesis: verum

proof

assume A24: p /. i = n + 1 ; :: thesis: i = q

per cases ( i = q or i < q or i > q ) by XXREAL_0:1;

suppose i = q ; :: thesis: i = q

hence i = q ; :: thesis: verum

end;

suppose i < q ; :: thesis: i = q

then n + 1 < q by A7, A23, A24;
hence i = q by A1, FINSEQ_1:3; :: thesis: verum

end;

suppose i > q ; :: thesis: i = q

then i - 1 = n + 1 by A7, A23, A24;
then i >= (n + 1) + 1 ;
then i > n + 1 by NAT_1:13;
hence i = q by A23, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

end;

A25: for i being Element of NAT st i in Seg (n + 1) & p /. i <> n + 1 holds
( i < q iff p /. i < q )

proof

let i be Element of NAT ; :: thesis: ( i in Seg (n + 1) & p /. i <> n + 1 implies ( i < q iff p /. i < q ) )
assume that
A26: i in Seg (n + 1) and
A27: p /. i <> n + 1 ; :: thesis: ( i < q iff p /. i < q )
thus ( i < q implies p /. i < q ) by A7, A26; :: thesis: ( p /. i < q implies i < q )
thus ( p /. i < q implies i < q ) :: thesis: verum

proof

assume A28: p /. i < q ; :: thesis: i < q

per cases ( i < q or i = q or i > q ) by XXREAL_0:1;

suppose i < q ; :: thesis: i < q

hence i < q ; :: thesis: verum

end;

suppose i = q ; :: thesis: i < q

hence i < q by A7, A26, A27; :: thesis: verum

end;

suppose A29: i > q ; :: thesis: i < q

then p /. i = i - 1 by A7, A26;
then (i - 1) + 1 < q + 1 by A28, XREAL_1:10;
hence i < q by A29, NAT_1:13; :: thesis: verum

end;

end;

end;

end;

for i1, i2 being set st i1 in Seg (n + 1) & i2 in Seg (n + 1) & p . i1 = p . i2 holds
i1 = i2

proof

let i1, i2 be set ; :: thesis: ( i1 in Seg (n + 1) & i2 in Seg (n + 1) & p . i1 = p . i2 implies i1 = i2 )
assume that
A30: i1 in Seg (n + 1) and
A31: i2 in Seg (n + 1) and
A32: p . i1 = p . i2 ; :: thesis: i1 = i2
reconsider i1 = i1 as Element of NAT by A30;
reconsider i2 = i2 as Element of NAT by A31;
A33: ( p /. i1 = p . i1 & p /. i2 = p . i2 ) by A6, A30, A31, PARTFUN1:def 8;

per cases ( p /. i1 = n + 1 or ( p /. i1 <> n + 1 & p /. i1 < q ) or ( p /. i1 <> n + 1 & p /. i1 >= q ) ) ;

suppose p /. i1 = n + 1 ; :: thesis: i1 = i2

then ( i1 = q & i2 = q ) by A22, A30, A31, A32, A33;
hence i1 = i2 ; :: thesis: verum

end;

suppose ( p /. i1 <> n + 1 & p /. i1 < q ) ; :: thesis: i1 = i2

then ( i1 < q & i2 < q ) by A25, A30, A31, A32, A33;
then ( p /. i1 = i1 & p /. i2 = i2 ) by A7, A30, A31;
hence i1 = i2 by A32, A33; :: thesis: verum

end;

suppose A34: ( p /. i1 <> n + 1 & p /. i1 >= q ) ; :: thesis: i1 = i2

then A35: ( i1 >= q & i2 >= q ) by A25, A30, A31, A32, A33;
( i1 <> q & i2 <> q ) by A22, A30, A31, A32, A33, A34;
then ( i1 > q & i2 > q ) by A35, XXREAL_0:1;
then ( p /. i1 = i1 - 1 & p /. i2 = i2 - 1 ) by A7, A30, A31;
hence i1 = i2 by A32, A33, XCMPLX_1:19; :: thesis: verum

end;

end;

end;

then X: p is one-to-one by A6, FUNCT_1:def 8;
p is Function of (Seg (n + 1)),(Seg (n + 1)) by A6, A21, FUNCT_2:3;
then reconsider p = p as Permutation of (Seg (n + 1)) by A21, X, FUNCT_2:83;
take p ; :: thesis: for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )
thus for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) by A8; :: thesis: verum