theorem :: MATRIX_1:8

for n being Nat ex P being non empty permutational set st len P = n