theorem Th15: :: MATRIX_1:15

for n being Nat holds idseq n = 1_ (Group_of_Perm n)