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 Def5;
hence ( p * (p ") = idseq n & (p ") * p = idseq n ) by FUNCT_2:61; :: thesis: verum