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