let A be non empty set ; :: thesis: for f being Permutation of A holds (id A) \ f = id A
let f be Permutation of A; :: thesis: (id A) \ f = id A
thus (id A) \ f = f * (f ") by FUNCT_2:17
.= id A by FUNCT_2:61 ; :: thesis: verum