let p be Permutation of (Seg 3); :: thesis: p * <*1,2,3*> = p
p is Element of Permutations 3 by MATRIX_2:def 9;
hence p * <*1,2,3*> = p by FINSEQ_2:53, MATRIX_2:21; :: thesis: verum