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:66
.= (((g * h) * f) * (h " )) * (g " ) by RELAT_1:55
.= ((g * (h * f)) * (h " )) * (g " ) by RELAT_1:55
.= (f \ h) \ g by RELAT_1:55 ; :: thesis: verum