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

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