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