let p be Permutation of Seg 3; :: thesis: <*1,2,3*> * p = p
p is Element of Permutations 3 by MATRIX_2:def 11;
hence <*1,2,3*> * p = p by FINSEQ_2:62, MATRIX_2:24; :: thesis: verum