let G be Group; :: thesis: for h, g being Element of G holds (h * g) " = (g " ) * (h " )
let h, g be Element of G; :: thesis: (h * g) " = (g " ) * (h " )
((g " ) * (h " )) * (h * g) = (((g " ) * (h " )) * h) * g by Def4
.= ((g " ) * ((h " ) * h)) * g by Def4
.= ((g " ) * (1_ G)) * g by Def6
.= (g " ) * g by Def5
.= 1_ G by Def6 ;
hence (h * g) " = (g " ) * (h " ) by Th20; :: thesis: verum