for n, i, j being Nat st i in Seg (n + 1) & j in Seg (n + 1) holds
card { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } = n !