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

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