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 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 & 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 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 ) ) ;
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 A4, FINSEQ_1:1;
then perm . k < n + 1 by A15, XXREAL_0:2;
then A16: perm . k <= n by NAT_1:13;
A17: S1[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 & 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 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: S1[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 & 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 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: S1[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 & 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 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: S1[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 & 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 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
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 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 ) ) ;
suppose A50: ( k1 < i & perm . k1 < perm . i ) ; :: thesis: x1 = x2
then A51: q . k1 = p9 . k1 by A31, A32, A36;
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 A2, A36, A43, A41, A47, FUNCT_1:def 4; :: thesis: verum
end;
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;
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;
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;
end;
end;
suppose A55: ( k1 < i & perm . k1 >= perm . i ) ; :: thesis: x1 = x2
then A56: q . k1 = (perm . k1) - 1 by A31, A32, A36;
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 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;
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;
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;
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 A2, A41, A49, FUNCT_1:def 4;
hence x1 = x2 by A55, A59, NAT_1:13; :: 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 A31, A32, A36;
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 A2, A47, A42, FUNCT_1:def 4;
hence x1 = x2 by A60, A62, NAT_1:13; :: 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 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;
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;
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;
end;
end;
suppose A65: ( k1 >= i & perm . (k1 + 1) >= perm . i ) ; :: thesis: x1 = x2
then A66: q . k1 = (perm . (k1 + 1)) - 1 by A31, A32, A36;
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 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;
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;
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;
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 A2, A42, A49, FUNCT_1:def 4;
hence x1 = x2 by A36, A43; :: thesis: verum
end;
end;
end;
end;
end;
then A70: q is one-to-one by FUNCT_1:def 4;
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