let h be Element of ; :: thesis: h " = - h
reconsider g = - h as Element of ;
h * g = 1_ INT.Group by Th35;
hence h " = - h by GROUP_1:20; :: thesis: verum