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 Def3
.= (g * ((h ") * (g "))) * h by Def3
.= (g * ((g ") * (h "))) * h by A1, Th18
.= ((g * (g ")) * (h ")) * h by Def3
.= ((1_ G) * (h ")) * h by Def5
.= (h ") * h by Def4
.= 1_ G by Def5 ;
then g * (h ") = ((g ") * h) " by Th11
.= (h ") * ((g ") ") by Th16 ;
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 Def3;
then g * (1_ G) = ((h ") * g) * h by Def5;
then g = ((h ") * g) * h by Def4;
then g = (h ") * (g * h) by Def3;
then h * g = (h * (h ")) * (g * h) by Def3;
then h * g = (1_ G) * (g * h) by Def5;
hence g * h = h * g by Def4; :: thesis: verum