let n, i, j be Nat; :: thesis: ( i in Seg (n + 1) & j in Seg (n + 1) implies card { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } = n ! )
assume that
A1: i in Seg (n + 1) and
A2: j in Seg (n + 1) ; :: thesis: card { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } = n !
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set n1 = N + 1;
set X = finSeg (N + 1);
set Y = (finSeg (N + 1)) \ {j};
A3: ((finSeg (N + 1)) \ {j}) \/ {j} = finSeg (N + 1) by A2, ZFMISC_1:116;
set X9 = (finSeg (N + 1)) \ {i};
set P1 = Permutations (N + 1);
set F = { p where p is Element of Permutations (N + 1) : p . i = j } ;
set F9 = { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) } ;
A4: ((finSeg (N + 1)) \ {i}) \/ {i} = finSeg (N + 1) by A1, ZFMISC_1:116;
A5: { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) } c= { p where p is Element of Permutations (N + 1) : p . i = j }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) } or x in { p where p is Element of Permutations (N + 1) : p . i = j } )
assume x in { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) } ; :: thesis: x in { p where p is Element of Permutations (N + 1) : p . i = j }
then consider f being Function of (finSeg (N + 1)),(finSeg (N + 1)) such that
A6: f = x and
A7: f is one-to-one and
A8: f . i = j by A4, A3;
card (finSeg (N + 1)) = card (finSeg (N + 1)) ;
then f is onto by A7, FINSEQ_4:63;
then f in Permutations (N + 1) by A7, MATRIX_1:def 12;
hence x in { p where p is Element of Permutations (N + 1) : p . i = j } by A6, A8; :: thesis: verum

end;

{ p where p is Element of Permutations (N + 1) : p . i = j } c= { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of Permutations (N + 1) : p . i = j } or x in { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) } )
assume x in { p where p is Element of Permutations (N + 1) : p . i = j } ; :: thesis: x in { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) }
then consider p being Element of Permutations (N + 1) such that
A9: x = p and
A10: p . i = j ;
reconsider p = p as Permutation of (finSeg (N + 1)) by MATRIX_1:def 12;
p . i = j by A10;
hence x in { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) } by A4, A3, A9; :: thesis: verum

end;

then A11: { p where p is Element of Permutations (N + 1) : p . i = j } = { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) } by A5, XBOOLE_0:def 10;
A12: card (finSeg (N + 1)) = N + 1 by FINSEQ_1:57;
A13: not j in (finSeg (N + 1)) \ {j} by ZFMISC_1:56;
then A14: card (finSeg (N + 1)) = (card ((finSeg (N + 1)) \ {j})) + 1 by A3, CARD_2:41;
A15: not i in (finSeg (N + 1)) \ {i} by ZFMISC_1:56;
then A16: card (finSeg (N + 1)) = (card ((finSeg (N + 1)) \ {i})) + 1 by A4, CARD_2:41;
then ( (finSeg (N + 1)) \ {j} is empty implies (finSeg (N + 1)) \ {i} is empty ) by A14;
hence card { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } = card { f where f is Function of ((finSeg (N + 1)) \ {i}),((finSeg (N + 1)) \ {j}) : f is one-to-one } by A15, A13, A11, CARD_FIN:5
.= ((card ((finSeg (N + 1)) \ {j})) !) / (((card ((finSeg (N + 1)) \ {j})) -' (card ((finSeg (N + 1)) \ {i}))) !) by A16, A14, CARD_FIN:7
.= ((card ((finSeg (N + 1)) \ {j})) !) / 1 by A16, A14, NEWTON:12, XREAL_1:232
.= n ! by A14, A12 ;
:: thesis: verum