theorem Th36: :: MATRIX_9:36

for n being Nat
for f being Permutation of (Seg n) holds f is FinSequence of Seg n