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

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