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