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 )
A1: ( Seg n = {} implies Seg n = {} ) ;
p is Permutation of (Seg n) by Def12;
then A2: rng p = Seg n by FUNCT_2:def 3;
p is Function of (Seg n),(Seg n) by Def12;
then dom p = Seg n by A1, FUNCT_2:def 1;
hence ( p * (idseq n) = p & (idseq n) * p = p ) by A2, RELAT_1:52, RELAT_1:54; :: thesis: verum