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 A1: ( i in Seg (n + 1) & 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 13;
set n1 = N + 1;
set X = finSeg (N + 1);
set P1 = Permutations (N + 1);
set F = { p where p is Element of Permutations (N + 1) : p . i = j } ;
set X' = (finSeg (N + 1)) \ {i};
set Y = (finSeg (N + 1)) \ {j};
set F' = { f where f is Function of (((finSeg (N + 1)) \ {i}) \/ {i}),(((finSeg (N + 1)) \ {j}) \/ {j}) : ( f is one-to-one & f . i = j ) } ;
A2: ( ((finSeg (N + 1)) \ {i}) \/ {i} = finSeg (N + 1) & ((finSeg (N + 1)) \ {j}) \/ {j} = finSeg (N + 1) & not i in (finSeg (N + 1)) \ {i} & not j in (finSeg (N + 1)) \ {j} ) by A1, ZFMISC_1:64, ZFMISC_1:140;
then A3: ( card (finSeg (N + 1)) = (card ((finSeg (N + 1)) \ {i})) + 1 & card (finSeg (N + 1)) = (card ((finSeg (N + 1)) \ {j})) + 1 & card (finSeg (N + 1)) = N + 1 ) by CARD_2:54, FINSEQ_1:78;
A4: { 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 set ; :: 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
A5: ( f = x & f is one-to-one & f . i = j ) by A2;
card (finSeg (N + 1)) = card (finSeg (N + 1)) ;
then f is onto by A5, STIRL2_1:70;
then f is Permutation of (finSeg (N + 1)) by A5;
then f in Permutations (N + 1) by MATRIX_2:def 11;
hence x in { p where p is Element of Permutations (N + 1) : p . i = j } by A5; :: 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 set ; :: 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
A6: ( x = p & p . i = j ) ;
reconsider p = p as Permutation of (finSeg (N + 1)) by MATRIX_2:def 11;
( p is one-to-one & p . i = j ) by A6;
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 A2, A6; :: thesis: verum

end;

then A7: { 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 A4, XBOOLE_0:def 10;
( (finSeg (N + 1)) \ {j} is empty implies (finSeg (N + 1)) \ {i} is empty ) by A3;
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 A2, A7, CARD_FIN:5
.= ((card ((finSeg (N + 1)) \ {j})) ! ) / (((card ((finSeg (N + 1)) \ {j})) -' (card ((finSeg (N + 1)) \ {i}))) ! ) by A3, CARD_FIN:7
.= ((card ((finSeg (N + 1)) \ {j})) ! ) / 1 by A3, NEWTON:18, XREAL_1:234
.= n ! by A3 ;
:: thesis: verum