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 Def5;

then A2: rng p = Seg n by FUNCT_2:def 3;

p is Function of (Seg n),(Seg n) by Def5;

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

( 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 Def5;

then A2: rng p = Seg n by FUNCT_2:def 3;

p is Function of (Seg n),(Seg n) by Def5;

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