:: deftheorem Def3 defines Rem LAPLACE:def 3 :
for i, n being Nat
for perm being Element of Permutations (n + 1) st i in Seg (n + 1) holds
for b₄ being Element of Permutations n holds
( b₄ = Rem (perm,i) iff for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b₄ . k = perm . k ) & ( perm . k >= perm . i implies b₄ . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b₄ . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b₄ . k = (perm . (k + 1)) - 1 ) ) ) ) );