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 " )
hence (g " ) * (h " ) = (g * h) " by Th25
.= (h " ) * (g " ) by A1, Th26 ;
:: thesis: verum

end;

assume A2: (g " ) * (h " ) = (h " ) * (g " ) ; :: thesis: g * h = h * g
thus g * h = ((g * h) " ) "
.= ((h " ) * (g " )) " by Th25
.= ((h " ) " ) * ((g " ) " ) by A2, Th25
.= h * g ; :: thesis: verum