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 S1[ 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 S1[i,p]
proof
let i be Nat; :: thesis: ( i in Seg (n + 1) implies ex p being Element of NAT st S1[i,p] )
assume i in Seg (n + 1) ; :: thesis: ex p being Element of NAT st S1[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 S1[i,p]
take i ; :: thesis: ( i is Element of NAT & S1[i,i] )
i in NAT by ORDINAL1:def 12;
hence ( i is Element of NAT & S1[i,i] ) by A3; :: thesis: verum
end;
suppose A4: i = q ; :: thesis: ex p being Element of NAT st S1[i,p]
take n + 1 ; :: thesis: S1[i,n + 1]
thus S1[i,n + 1] by A4; :: thesis: verum
end;
suppose A5: i > q ; :: thesis: ex p being Element of NAT st S1[i,p]
1 <= q by ;
then reconsider p = i - 1 as Element of NAT by ;
take p ; :: thesis: S1[i,p]
thus S1[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
S1[i,p /. i] from 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 ; :: 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 ; :: 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 ;
hence ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) by ; :: 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 ;
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 ; :: thesis: verum
end;
suppose j = q ; :: thesis: i in Seg (n + 1)
then i = n + 1 by ;
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 ;
A17: 1 <= q by ;
then reconsider i = i as Element of NAT by ;
j <= n + 1 by ;
then i <= n by ;
then A18: i <= n + 1 by NAT_1:12;
1 < i + 1 by ;
then 1 <= i by NAT_1:13;
hence i in Seg (n + 1) by ; :: 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 ;
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 ;
suppose i < q ; :: thesis: i in rng p
then p . i = i by ;
hence i in rng p by ; :: 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 ;
then A23: i + 1 in Seg (n + 1) by ;
q < i + 1 by ;
then p . (i + 1) = (i + 1) - 1 by
.= i ;
hence i in rng p by ; :: thesis: verum
end;
suppose i = n + 1 ; :: thesis: i in rng p
then p . q = i by ;
hence i in rng p by ; :: 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 ;
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 ; :: 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 ;
then (i - 1) + 1 < q + 1 by ;
hence i < q by ; :: 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 ;
reconsider i2 = i2 as Element of NAT by A32;
A35: p /. i2 = p . i2 by ;
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 ;
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 ;
then A38: p /. i1 = i1 by ;
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 ;
i1 >= q by ;
then i1 > q by ;
then A41: p /. i1 = i1 - 1 by ;
A42: i2 <> q by A8, A32, A33, A34, A35, A39;
i2 >= q by A26, A32, A33, A34, A35, A39;
then i2 > q by ;
then p /. i2 = i2 - 1 by ;
hence i1 = i2 by ; :: thesis: verum
end;
end;
end;
then p is one-to-one by ;
then reconsider p = p as Permutation of (Seg (n + 1)) by ;
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