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:66
.= ((g " ) " ) * ((f " ) * (g " )) by FUNCT_1:66
.= g * ((f " ) * (g " )) by FUNCT_1:65
.= (f " ) \ g by RELAT_1:55 ; :: thesis: verum