let A be non empty set ; :: thesis: for g, f, h being Permutation of A st g * f = h * f holds
g = h
let g, f, 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:55;
then g * (f * (f " )) = h * (f * (f " )) by RELAT_1:55;
then g * (id A) = h * (f * (f " )) by FUNCT_2:88;
then g * (id A) = h * (id A) by FUNCT_2:88;
then g = h * (id A) by FUNCT_2:23;
hence g = h by FUNCT_2:23; :: thesis: verum