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