let G be Group; :: thesis: for g, h being Element of G holds
( g * h = h * g iff (g * h) " = (g ") * (h ") )
let g, h be Element of G; :: thesis: ( g * h = h * g iff (g * h) " = (g ") * (h ") )
thus ( g * h = h * g implies (g * h) " = (g ") * (h ") ) by Th16; :: thesis: ( (g * h) " = (g ") * (h ") implies g * h = h * g )
assume (g * h) " = (g ") * (h ") ; :: thesis: g * h = h * g
then A1: (h * g) * ((g * h) ") = ((h * g) * (g ")) * (h ") by Def3
.= (h * (g * (g "))) * (h ") by Def3
.= (h * (1_ G)) * (h ") by Def5
.= h * (h ") by Def4
.= 1_ G by Def5 ;
(g * h) * ((g * h) ") = 1_ G by Def5;
hence g * h = h * g by A1, Th6; :: thesis: verum