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 }

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

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

{ 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 ) }
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;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

proof

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;
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;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

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