theorem Th39: :: MATRIX_9:39

for n being Nat
for f, g being Element of Permutations n holds f * g in Permutations n