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