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