theorem Th11: :: MATRIX_1:11

for n being Nat holds idseq n is Element of (Group_of_Perm n)