let A be non empty set ; :: thesis: for f, g, h being Permutation of A st f * g = f * h holds
g = h
let f, g, h be Permutation of A; :: thesis: ( f * g = f * h implies g = h )
assume f * g = f * h ; :: thesis: g = h
then ((f ") * f) * g = (f ") * (f * h) by RELAT_1:36;
then ((f ") * f) * g = ((f ") * f) * h by RELAT_1:36;
then (id A) * g = ((f ") * f) * h by FUNCT_2:61;
then (id A) * g = (id A) * h by FUNCT_2:61;
then g = (id A) * h by FUNCT_2:17;
hence g = h by FUNCT_2:17; :: thesis: verum