let G be Group; :: thesis: for g, h being Element of G holds
( g * h = h * g iff g * (h ") = (h ") * g )
let g, h be Element of G; :: thesis: ( g * h = h * g iff g * (h ") = (h ") * g )
thus ( g * h = h * g implies g * (h ") = (h ") * g ) :: thesis: ( g * (h ") = (h ") * g implies g * h = h * g )

proof

assume A1: g * h = h * g ; :: thesis: g * (h ") = (h ") * g
(g * (h ")) * ((g ") * h) = ((g * (h ")) * (g ")) * h by Def4
.= (g * ((h ") * (g "))) * h by Def4
.= (g * ((g ") * (h "))) * h by A1, Th27
.= ((g * (g ")) * (h ")) * h by Def4
.= ((1_ G) * (h ")) * h by Def6
.= (h ") * h by Def5
.= 1_ G by Def6 ;
then g * (h ") = ((g ") * h) " by Th20
.= (h ") * ((g ") ") by Th25 ;
hence g * (h ") = (h ") * g ; :: thesis: verum

end;

assume g * (h ") = (h ") * g ; :: thesis: g * h = h * g
then g * ((h ") * h) = ((h ") * g) * h by Def4;
then g * (1_ G) = ((h ") * g) * h by Def6;
then g = ((h ") * g) * h by Def5;
then g = (h ") * (g * h) by Def4;
then h * g = (h * (h ")) * (g * h) by Def4;
then h * g = (1_ G) * (g * h) by Def6;
hence g * h = h * g by Def5; :: thesis: verum