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

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