now :: thesis: for a, b, c being Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) holds (a * b) * c = a * (b * c)

let a, b, c be Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #); :: thesis: (a * b) * c = a * (b * c)
reconsider x = a, y = b, z = c as Element of L ;
thus (a * b) * c = (x * y) * z
.= x * (y * z) by GROUP_1:def 3
.= a * (b * c) ; :: thesis: verum

end;

hence doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is associative ; :: thesis: verum