let GS be non empty addLoopStr ; :: thesis: ( the addF of GS is commutative & the addF of GS is associative implies ( GS is Abelian & GS is add-associative ) )
assume that
A1: the addF of GS is commutative and
A2: the addF of GS is associative ; :: thesis: ( GS is Abelian & GS is add-associative )
thus GS is Abelian :: thesis: GS is add-associative

proof

let x, y be Element of GS; :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
thus x + y = y + x by A1, BINOP_1:def 2; :: thesis: verum

end;

let x, y, z be Element of GS; :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = x + (y + z) by A2, BINOP_1:def 3; :: thesis: verum