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

( 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