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 ) ) )
defpred S₁[ Nat, set ] means ( ( $1 < q implies $2 = $1 ) & ( $1 = q implies $2 = n + 1 ) & ( $1 > q implies $2 = $1 - 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 ) )
A2: for i being Nat st i in Seg (n + 1) holds
ex p being Element of NAT st S₁[i,p]

proof

let i be 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: ( i is Element of NAT & S₁[i,i] )
i in NAT by ORDINAL1:def 12;
hence ( i is Element of NAT & 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:1;
then reconsider p = i - 1 as Element of NAT by A5, INT_1:5, 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 Nat st i in Seg (n + 1) holds
S₁[i,p /. i] from RECDEF_1:sch 17(A2);
A8: 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 A9: 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 A10: 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, A9, A10;
hence i = q by A1, FINSEQ_1:1; :: thesis: verum

end;

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

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

end;

end;

end;

end;

A11: 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 A12: 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 6;
hence ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) by A7, A12; :: thesis: verum

end;

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

proof

let i be object ; :: 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 object such that
A13: j in Seg (n + 1) and
A14: p . j = i by A6, FUNCT_1:def 3;
reconsider j = j as Element of NAT by A13;

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 A11, A13, A14; :: thesis: verum

end;

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

then i = n + 1 by A11, A13, A14;
hence i in Seg (n + 1) by FINSEQ_1:4; :: thesis: verum

end;

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

then A16: i = j - 1 by A11, A13, A14;
A17: 1 <= q by A1, FINSEQ_1:1;
then reconsider i = i as Element of NAT by A15, A16, INT_1:5, XXREAL_0:2;
j <= n + 1 by A13, FINSEQ_1:1;
then i <= n by A16, XREAL_1:20;
then A18: i <= n + 1 by NAT_1:12;
1 < i + 1 by A15, A16, A17, XXREAL_0:2;
then 1 <= i by NAT_1:13;
hence i in Seg (n + 1) by A18, FINSEQ_1:1; :: thesis: verum

end;

end;

end;

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

proof

assume A19: i in Seg (n + 1) ; :: thesis: i in rng p
then reconsider i = i as Element of NAT ;
i <= n + 1 by A19, FINSEQ_1:1;
then A20: ( 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 A20, NAT_1:13;

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

then p . i = i by A11, A19;
hence i in rng p by A6, A19, FUNCT_1:3; :: thesis: verum

end;

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

A22: 1 <= i + 1 by NAT_1:12;
i + 1 <= n + 1 by A21, XREAL_1:6;
then A23: i + 1 in Seg (n + 1) by A22, FINSEQ_1:1;
q < i + 1 by A21, NAT_1:13;
then p . (i + 1) = (i + 1) - 1 by A11, A23
.= i ;
hence i in rng p by A6, A23, FUNCT_1:3; :: thesis: verum

end;

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

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

end;

end;

end;

end;

then A24: rng p = Seg (n + 1) by TARSKI:2;
then A25: p is Function of (Seg (n + 1)),(Seg (n + 1)) by A6, FUNCT_2:1;
A26: 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
A27: i in Seg (n + 1) and
A28: p /. i <> n + 1 ; :: thesis: ( i < q iff p /. i < q )
thus ( i < q implies p /. i < q ) by A7, A27; :: thesis: ( p /. i < q implies i < q )
thus ( p /. i < q implies i < q ) :: thesis: verum

proof

assume A29: 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, A27, A28; :: thesis: verum

end;

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

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

end;

end;

end;

end;

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

proof

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

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

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

then i1 = q by A8, A31;
hence i1 = i2 by A8, A32, A33, A34, A35, A36; :: thesis: verum

end;

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

then i1 < q by A26, A31;
then A38: p /. i1 = i1 by A7, A31;
i2 < q by A26, A32, A33, A34, A35, A37;
hence i1 = i2 by A7, A32, A33, A34, A35, A38; :: thesis: verum

end;

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

then A40: i1 <> q by A8, A31;
i1 >= q by A26, A31, A39;
then i1 > q by A40, XXREAL_0:1;
then A41: p /. i1 = i1 - 1 by A7, A31;
A42: i2 <> q by A8, A32, A33, A34, A35, A39;
i2 >= q by A26, A32, A33, A34, A35, A39;
then i2 > q by A42, XXREAL_0:1;
then p /. i2 = i2 - 1 by A7, A32;
hence i1 = i2 by A6, A32, A33, A34, A41, PARTFUN1:def 6, XCMPLX_1:19; :: thesis: verum

end;

end;

end;

then p is one-to-one by A6, FUNCT_1:def 4;
then reconsider p = p as Permutation of (Seg (n + 1)) by A24, A25, FUNCT_2:57;
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 A11; :: thesis: verum