let p be Permutation of (Seg 3); :: thesis: <*1,2,3*> * p = p

p is Element of Permutations 3 by MATRIX_1:def 12;

hence <*1,2,3*> * p = p by FINSEQ_2:53, MATRIX_1:12; :: thesis: verum

p is Element of Permutations 3 by MATRIX_1:def 12;

hence <*1,2,3*> * p = p by FINSEQ_2:53, MATRIX_1:12; :: thesis: verum