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