let A be non empty set ; :: thesis: for f, g being Permutation of A holds (f ") \ g = (f \ g) "
let f, g be Permutation of A; :: thesis: (f ") \ g = (f \ g) "
thus (f \ g) " = ((g ") ") * ((g * f) ") by FUNCT_1:44
.= ((g ") ") * ((f ") * (g ")) by FUNCT_1:44
.= g * ((f ") * (g ")) by FUNCT_1:43
.= (f ") \ g by RELAT_1:36 ; :: thesis: verum