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

end;

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