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 Th25; :: 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 Def4
.= (h * (g * (g "))) * (h ") by Def4
.= (h * (1_ G)) * (h ") by Def6
.= h * (h ") by Def5
.= 1_ G by Def6 ;
(g * h) * ((g * h) ") = 1_ G by Def6;
hence g * h = h * g by A1, Th14; :: thesis: verum