theorem Th9: :: MATRIX_1:9

for n being Nat holds len (Permutations n) = n