theorem Th18: :: MATRIX_9:18

for n being Nat
for f, g being FinSequence st f ^ g in Permutations n holds
g ^ f in Permutations n