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