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

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