let A be non empty set ; :: thesis: for f, g, h being Permutation of A holds f \ (g * h) = (f \ h) \ g
let f, g, h be Permutation of A; :: thesis: f \ (g * h) = (f \ h) \ g
thus f \ (g * h) = ((g * h) * f) * ((h ") * (g ")) by FUNCT_1:44
.= (((g * h) * f) * (h ")) * (g ") by RELAT_1:36
.= ((g * (h * f)) * (h ")) * (g ") by RELAT_1:36
.= (f \ h) \ g by RELAT_1:36 ; :: thesis: verum