theorem Th2: :: MATRIX_9:2

( (Rev (idseq 2)) . 1 = 2 & (Rev (idseq 2)) . 2 = 1 )