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