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 S1[ 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 ;
A5: for k9 being object st k9 in Seg n holds
ex y being object st
( y in Seg n & S1[k9,y] )
proof
let k9 be object ; :: thesis: ( k9 in Seg n implies ex y being object st
( y in Seg n & S1[k9,y] ) )

assume k9 in Seg n ; :: thesis: ex y being object st
( y in Seg n & S1[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 ;
then A10: k in Seg (n + 1) by A7;
then A11: perm . k in Seg (n + 1) by ;
set k1 = k + 1;
A12: 1 + 0 <= k + 1 by NAT_1:13;
k + 1 <= n + 1 by ;
then A13: k + 1 in Seg (n + 1) by A12;
then A14: perm . (k + 1) in Seg (n + 1) by ;
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 ) ) ;
suppose A15: ( k < i & perm . k < perm . i ) ; :: thesis: ex y being object st
( y in Seg n & S1[k9,y] )

perm . i <= n + 1 by ;
then perm . k < n + 1 by ;
then A16: perm . k <= n by NAT_1:13;
A17: S1[k9,perm . k] by ;
1 <= perm . k by ;
then perm . k in Seg n by A16;
hence ex y being object st
( y in Seg n & S1[k9,y] ) by A17; :: thesis: verum
end;
suppose A18: ( k < i & perm . k >= perm . i ) ; :: thesis: ex y being object st
( y in Seg n & S1[k9,y] )

then p9 . k <> p9 . i by ;
then A19: perm . k > perm . i by ;
then reconsider pk1 = (perm . k) - 1 as Element of NAT by NAT_1:20;
A20: S1[k9,pk1] by A6, A18;
A21: pk1 < pk1 + 1 by NAT_1:13;
perm . k <= n + 1 by ;
then pk1 < n + 1 by ;
then A22: pk1 <= n by NAT_1:13;
perm . i >= 1 by ;
then pk1 + 1 > 1 by ;
then pk1 >= 1 by NAT_1:13;
then pk1 in Seg n by A22;
hence ex y being object st
( y in Seg n & S1[k9,y] ) by A20; :: thesis: verum
end;
suppose A23: ( k >= i & perm . (k + 1) < perm . i ) ; :: thesis: ex y being object st
( y in Seg n & S1[k9,y] )

perm . i <= n + 1 by ;
then perm . (k + 1) < n + 1 by ;
then A24: perm . (k + 1) <= n by NAT_1:13;
A25: S1[k9,perm . (k + 1)] by ;
1 <= perm . (k + 1) by ;
then perm . (k + 1) in Seg n by A24;
hence ex y being object st
( y in Seg n & S1[k9,y] ) by A25; :: thesis: verum
end;
suppose A26: ( k >= i & perm . (k + 1) >= perm . i ) ; :: thesis: ex y being object st
( y in Seg n & S1[k9,y] )

then i < k + 1 by NAT_1:13;
then p9 . (k + 1) <> p9 . i by ;
then A27: perm . (k + 1) > perm . i by ;
then reconsider pk1 = (perm . (k + 1)) - 1 as Element of NAT by NAT_1:20;
A28: S1[k9,pk1] by A6, A26;
A29: pk1 < pk1 + 1 by NAT_1:13;
perm . (k + 1) <= n + 1 by ;
then pk1 < n + 1 by ;
then A30: pk1 <= n by NAT_1:13;
perm . i >= 1 by ;
then pk1 + 1 > 1 by ;
then pk1 >= 1 by NAT_1:13;
then pk1 in Seg n by A30;
hence ex y being object st
( y in Seg n & S1[k9,y] ) by A28; :: thesis: verum
end;
end;
end;
consider q being Function of (Seg n),(Seg n) such that
A31: for x being object st x in Seg n holds
S1[x,q . x] from for x1, x2 being object st x1 in dom q & x2 in dom q & q . x1 = q . x2 holds
x1 = x2
proof
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 ;
then A41: k1 in Seg (n + 1) by A37;
k1 + 1 <= n + 1 by ;
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 ;
A46: k2 < n + 1 by ;
then A47: k2 in Seg (n + 1) by A44;
A48: 0 + 1 <= k2 + 1 by NAT_1:13;
k2 + 1 <= n + 1 by ;
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 ) ) ;
suppose A50: ( k1 < i & perm . k1 < perm . i ) ; :: thesis: x1 = x2
then A51: q . k1 = p9 . k1 by ;
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 ) ) ;
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 ; :: thesis: verum
end;
suppose A52: ( k2 < i & perm . k2 >= perm . i ) ; :: thesis: x1 = x2
then q . k2 = (perm . k2) - 1 by ;
then (perm . k1) + 1 = perm . k2 by A34, A36, A43, A51;
then perm . k2 <= perm . i by ;
then p9 . k2 = p9 . i by ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
then p9 . (k2 + 1) = perm . i by ;
then k2 + 1 = i by ;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
suppose A55: ( k1 < i & perm . k1 >= perm . i ) ; :: thesis: x1 = x2
then A56: q . k1 = (perm . k1) - 1 by ;
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 ) ) ;
suppose A57: ( k2 < i & perm . k2 < perm . i ) ; :: thesis: x1 = x2
then q . k2 = p9 . k2 by ;
then perm . k1 = (perm . k2) + 1 by A34, A36, A43, A56;
then perm . k1 <= perm . i by ;
then perm . k1 = perm . i by ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ; :: thesis: verum
end;
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 ;
then p9 . k1 = p9 . i by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A59: ( k2 >= i & perm . (k2 + 1) >= perm . i ) ; :: thesis: x1 = x2
then (perm . k1) - 1 = (perm . (k2 + 1)) - 1 by A31, A33, A34, A36, A43, A56;
then k1 = k2 + 1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
suppose A60: ( k1 >= i & perm . (k1 + 1) < perm . i ) ; :: thesis: x1 = x2
then A61: q . k1 = perm . (k1 + 1) by ;
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 ) ) ;
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 ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
then p9 . k2 = p9 . i by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose ( k2 >= i & perm . (k2 + 1) < perm . i ) ; :: thesis: x1 = x2
then q . k2 = perm . (k2 + 1) by ;
then k1 + 1 = k2 + 1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
then p9 . (k2 + 1) = p9 . i by ;
then k2 + 1 = i by ;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
suppose A65: ( k1 >= i & perm . (k1 + 1) >= perm . i ) ; :: thesis: x1 = x2
then A66: q . k1 = (perm . (k1 + 1)) - 1 by ;
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 ) ) ;
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 ;
then p9 . (k1 + 1) = p9 . i by ;
then k1 + 1 = i by ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
then p9 . (k1 + 1) = p9 . i by ;
then k1 + 1 = i by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose ( k2 >= i & perm . (k2 + 1) >= perm . i ) ; :: thesis: x1 = x2
then (perm . (k1 + 1)) - 1 = (perm . (k2 + 1)) - 1 by A31, A33, A34, A36, A43, A66;
then k1 + 1 = k2 + 1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
end;
end;
then A70: q is one-to-one by FUNCT_1:def 4;
card () = card () ;
then ( q is one-to-one & q is onto ) by ;
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