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

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