let F be AbGroup; :: thesis: for a being Element of ex b being Element of st
( a + b = 0. F & b + a = 0. F )
let a be Element of ; :: thesis: ex b being Element of st
( a + b = 0. F & b + a = 0. F )
consider b being Element of such that
A1: a + b = 0. F by ALGSTR_0:def 11;
take b ; :: thesis: ( a + b = 0. F & b + a = 0. F )
thus a + b = 0. F by A1; :: thesis: b + a = 0. F
thus b + a = 0. F by A1; :: thesis: verum