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

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