deffunc H₁( addLoopStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1;
let LS be non empty addLoopStr ; :: thesis: ( the addF of LS is commutative & the addF of LS is associative implies ( LS is Abelian & LS is add-associative ) )
assume that
A1: H₁(LS) is commutative and
A2: H₁(LS) is associative ; :: thesis: ( LS is Abelian & LS is add-associative )
for x, y being Element of LS holds x + y = y + x by A1, BINOP_1:def 2;
hence LS is Abelian by RLVECT_1:def 5; :: thesis: LS is add-associative
for x, y, z being Element of LS holds (x + y) + z = x + (y + z) by A2, BINOP_1:def 3;
hence LS is add-associative by RLVECT_1:def 6; :: thesis: verum