let n be Nat; :: thesis: for p being Element of Permutations n holds
( p * (idseq n) = p & (idseq n) * p = p )
let p be Element of Permutations n; :: thesis: ( p * (idseq n) = p & (idseq n) * p = p )
p is Permutation of (Seg n) by Def11;
then A1: rng p = Seg n by FUNCT_2:def 3;
A2: p is Function of (Seg n),(Seg n) by Def11;
( Seg n = {} implies Seg n = {} ) ;
then dom p = Seg n by A2, FUNCT_2:def 1;
hence ( p * (idseq n) = p & (idseq n) * p = p ) by A1, RELAT_1:78, RELAT_1:80; :: thesis: verum