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 ) 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