let n be Nat; :: thesis: for p being Element of Permutations n holds
( p * (p " ) = idseq n & (p " ) * p = idseq n )
let p be Element of Permutations n; :: thesis: ( p * (p " ) = idseq n & (p " ) * p = idseq n )
p is Permutation of (Seg n) by Def11;
hence ( p * (p " ) = idseq n & (p " ) * p = idseq n ) by FUNCT_2:88; :: thesis: verum